Demostrar con Lean4 que las clases de equivalencia de elementos no relacionados son disjuntas.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {X : Type} variable {x y: X} variable {R : X → X → Prop} def clase (R : X → X → Prop) (x : X) := {y : X | R x y} example (h : Equivalence R) (hxy : ¬ R x y) : clase R x ∩ clase R y = ∅ := by sorry
Demostrar con Lean4 que las clases de equivalencia de elementos relacionados son iguales.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {X : Type} variable {x y: X} variable {R : X → X → Prop} def clase (R : X → X → Prop) (x : X) := {y : X | R x y} example (h : Equivalence R) (hxy : R x y) : clase R x = clase R y := by sorry
En Lean4, una sucesión \(u_0, u_1, u_2, ...\) se puede representar mediante una función \(u : ℕ → ℝ\) de forma que \(u(n)\) es \(uₙ\).
Se define
def limite (u : ℕ → ℝ) (a : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| ≤ ε
def suc_convergente (u : ℕ → ℝ) := ∃ a, limite u a
def suc_Cauchy (u : ℕ → ℝ) := ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| ≤ ε
Demostrar con Lean4 que las sucesiones convergentes son de Cauchy.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {u : ℕ → ℝ } def limite (u : ℕ → ℝ) (a : ℝ) : Prop := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - a| < ε def suc_convergente (u : ℕ → ℝ) := ∃ a, limite u a def suc_Cauchy (u : ℕ → ℝ) := ∀ ε > 0, ∃ N, ∀ p ≥ N, ∀ q ≥ N, |u p - u q| < ε example (h : suc_convergente u) : suc_Cauchy u := by sorry
Sean \(f_1\) y \(f_2\) funciones de \(X\) en \(Y\) y \(g\) una función de \(Y\) en \(Z\). Demostrar con Lean4 que si \(g\) es inyectiva y \(g ∘ f_1 = g ∘ f_2\), entonces \(f_1 = f_2\).
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Function variable {X Y Z : Type _} variable {f₁ f₂ : X → Y} variable {g : Y → Z} example (hg : Injective g) (hgf : g ∘ f₁ = g ∘ f₂) : f₁ = f₂ := by sorry
Sean \(X\) e \(Y\) dos conjuntos y \(f\) una función de \(X\) en \(Y\). Se define la relación \(\text{R}\) en \(X\) de forma que \(x\) está relacionado con \(y\) si \(f(x) = f(y)\).
Demostrar con Lean4 que \(\text{R}\) es una relación de equivalencia.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic variable {X Y : Type _} variable (f : X → Y) def R (x y : X) := f x = f y example : Equivalence (R f) := by sorry
Dos conjuntos \(A\) y \(B\) son equipotentes (y se denota por \(A ≃ B\)) si existe una aplicación biyectiva entre ellos. La equipotencia se puede definir en Lean4 por
def es_equipotente (A B : Type _) : Prop := ∃ g : A → B, Bijective g local infixr:50 " ⋍ " => es_equipotente
Demostrar con Lean4 que la relación de equipotencia es simétrica.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Function def es_equipotente (A B : Type _) := ∃ g : A → B, Bijective g local infixr:50 " ⋍ " => es_equipotente variable {X Y : Type _} variable {f : X → Y} variable {g : Y → X} def inversa (f : X → Y) (g : Y → X) := (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y) def tiene_inversa (f : X → Y) := ∃ g, inversa g f lemma aux1 (hf : Bijective f) : tiene_inversa f := by cases' (bijective_iff_has_inverse.mp hf) with g hg -- g : Y → X -- hg : LeftInverse g f ∧ Function.RightInverse g f aesop (add norm unfold [tiene_inversa, inversa]) lemma aux2 (hg : inversa g f) : Bijective g := by apply bijective_iff_has_inverse.mpr -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g exact ⟨f, hg⟩ example : Equivalence (. ⋍ .) := by sorry
Dos conjuntos \(A\) y \(B\) son equipotentes (y se denota por \(A ≃ B\)) si existe una aplicación biyectiva entre ellos. La equipotencia se puede definir en Lean4 por
def es_equipotente (A B : Type _) : Prop := ∃ g : A → B, Bijective g local infixr:50 " ⋍ " => es_equipotente
Demostrar con Lean4 que la relación de equipotencia es transitiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Function def es_equipotente (A B : Type _) := ∃ g : A → B, Bijective g local infixr:50 " ⋍ " => es_equipotente example : Transitive (. ⋍ .) := by sorry
Demostrar con Lean4 que la composición de dos funciones biyectivas es una función biyectiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Function variable {X Y Z : Type} variable {f : X → Y} variable {g : Y → Z} example (Hf : Bijective f) (Hg : Bijective g) : Bijective (g ∘ f) := by sorry
Dos conjuntos \(A\) y \(B\) son equipotentes (y se denota por \(A ≃ B\)) si existe una aplicación biyectiva entre ellos. La equipotencia se puede definir en Lean4 por
def es_equipotente (A B : Type _) : Prop := ∃ g : A → B, Bijective g local infixr:50 " ⋍ " => es_equipotente
Demostrar con Lean4 que la relación de equipotencia es simétrica.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Function def es_equipotente (A B : Type _) : Prop := ∃ g : A → B, Bijective g local infixr:50 " ⋍ " => es_equipotente def inversa (f : X → Y) (g : Y → X) := (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y) def tiene_inversa (f : X → Y) := ∃ g, inversa g f lemma aux1 (hf : Bijective f) : tiene_inversa f := by cases' (bijective_iff_has_inverse.mp hf) with g hg -- g : Y → X -- hg : LeftInverse g f ∧ Function.RightInverse g f aesop (add norm unfold [tiene_inversa, inversa]) lemma aux2 (hg : inversa g f) : Bijective g := by rw [bijective_iff_has_inverse] -- ⊢ ∃ g_1, LeftInverse g_1 g ∧ Function.RightInverse g_1 g exact ⟨f, hg⟩ example : Symmetric (. ⋍ .) := by sorry
En Lean4 se puede definir que \(g\) es una inversa de \(f\) por
def inversa (f : X → Y) (g : Y → X) := (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y)
Demostrar con Lean4 que si \(g\) es una inversa de \(f\), entonces \(g\) es biyectiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Function variable {X Y : Type _} variable (f : X → Y) variable (g : Y → X) def inversa (f : X → Y) (g : Y → X) := (∀ x, (g ∘ f) x = x) ∧ (∀ y, (f ∘ g) y = y) example (hg : inversa g f) : Bijective g := by sorry