Demostrar con Lean4 que un número es par si y solo si lo es su cuadrado.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Even import Mathlib.Tactic open Int variable (n : ℤ) example : Even (n^2) ↔ Even n := by sorry
Sea \(u\) una sucesión creciente. Demostrar con Lean4 que si \(S\) es un supremo de \(u\), entonces el límite de \(u\) es \(S\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable (u : ℕ → ℝ) variable (S : ℝ) -- (limite u c) expresa que el límite de u es c. def limite (u : ℕ → ℝ) (c : ℝ) := ∀ ε > 0, ∃ m, ∀ n ≥ m, |u n - c| ≤ ε -- (supremo u S) expresa que el supremo de u es S. def supremo (u : ℕ → ℝ) (S : ℝ) := (∀ n, u n ≤ S) ∧ ∀ ε > 0, ∃ k, u k ≥ S - ε example (hu : Monotone u) (hS : supremo u S) : limite u S := by sorry
Demostrar con Lean4 que si \(f\) una función de \(ℝ\) en \(ℝ\) tal que \[ (∀ x, y)[f(x) ≤ f(y) → x ≤ y] \] entonces \(f\) es inyectiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic open Function variable (f : ℝ → ℝ) example (h : ∀ {x y}, f x ≤ f y → x ≤ y) : Injective f := by sorry
Sea una función \(f\) de \(ℝ\) en \(ℝ\).
En Lean4 que \(f\) sea creciente se representa por Monotone f y que sea involutiva por Involutive f
Demostrar con Lean4 que si \(f\) es creciente e involutiva, entonces \(f\) es la identidad.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic open Function variable (f : ℝ → ℝ) example (hc : Monotone f) (hi : Involutive f) : f = id := by sorry
Sea una función \(f\) de \(ℝ\) en \(ℝ\). Se dice que \(f\) es creciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≤ f(y)\). Se dice que \(f\) es decreciente si para todo \(x\) e \(y\) tales que \(x ≤ y\) se tiene que \(f(x) ≥ f(y)\).
Demostrar con Lean4 que si \(f\) es creciente y \(g\) es decreciente, entonces \(g ∘ f\) es decreciente.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic variable (f g : ℝ → ℝ) def creciente (f : ℝ → ℝ) : Prop := ∀ {x y}, x ≤ y → f x ≤ f y def decreciente (f : ℝ → ℝ) : Prop := ∀ {x y}, x ≤ y → f x ≥ f y example (hf : creciente f) (hg : decreciente g) : decreciente (g ∘ f) := by sorry
Un monoide es un conjunto junto con una operación binaria que es asociativa y tiene elemento neutro.
Un monoide \(M\) es booleano si \[ (∀ x ∈ M)[x·x = 1] \] y es conmutativo si \[ (∀ x, y ∈ M)[x·y = y·x] \]
En Lean4, está definida la clase de los monoides (como Monoid) y sus propiedades características son
mul_assoc : (a * b) * c = a * (b * c) one_mul : 1 * a = a mul_one : a * 1 = a
Demostrar con Lean4 que los monoides booleanos son conmutativos.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Basic variable {M : Type} [Monoid M] example (h : ∀ x : M, x * x = 1) : ∀ x y : M, x * y = y * x := by sorry
Demostrar con Lean4 que si \(M\) es un monoide, \(a ∈ M\) y \(m, n ∈ ℕ\), entonces \[ a^{m·n} = (a^m)^n \]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Defs import Mathlib.Tactic open Nat variable {M : Type} [Monoid M] variable (a : M) variable (m n : ℕ) example : a^(m * n) = (a^m)^n := by sorry
Demostrar con Lean4 que si \(G\) es un grupo y \(a, b, c ∈ G\) tales que \(a·b = a·c\), entonces \(b = c\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a b c : G} example (h: a * b = a * c) : b = c := sorry
Demostrar con Lean4 que si \(G\) un grupo y \(a ∈ G\), entonces \[(a⁻¹)⁻¹ = a\]
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Basic variable {G : Type} [Group G] variable {a : G} example : (a⁻¹)⁻¹ = a := sorry
Demostrar con Lean4 que si \(G\) es un grupo y \(a, b \in G\), entonces \((ab)^{-1} = b^{-1}a^{-1}\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Algebra.Group.Defs variable {G : Type _} [Group G] variable (a b : G) example : (a * b)⁻¹ = b⁻¹ * a⁻¹ := sorry