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
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 Lean por
def es_equipotente (A B : Type _) : Prop := ∃ g : A → B, Bijective g local infixr:50 " ⋍ " => es_equipotente
Demostrar que la relación de equipotencia es reflexiva.
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 example : Reflexive (. ⋍ .) := 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)
y que \(f\) tiene inversa por
def tiene_inversa (f : X → Y) := ∃ g, inversa f g
Demostrar con Lean4 que si la función \(f\) es biyectiva, entonces \(f\) tiene inversa.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Function variable {X Y : Type _} variable (f : X → Y) 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 example (hf : Bijective f) : tiene_inversa f := 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)
y que \(f\) tiene inversa por
def tiene_inversa (f : X → Y) := ∃ g, inversa g f
Demostrar con Lean4 que si la función \(f\) tiene inversa, entonces \(f\) es biyectiva.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Function variable {X Y : Type _} variable (f : X → Y) 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 example (hf : tiene_inversa f) : Bijective f := by sorry
En Lean4, que \(g\) es una inversa por la izquierda de \(f\) está definido por
LeftInverse (g : β → α) (f : α → β) : Prop := ∀ x, g (f x) = x
que \(g\) es una inversa por la derecha de \(f\) está definido por
RightInverse (g : β → α) (f : α → β) : Prop := LeftInverse f g
y que \(f\) tenga inversa por la derecha está definido por
HasRightInverse (f : α → β) : Prop := ∃ g : β → α, RightInverse g f
Finalmente, que \(f\) es suprayectiva está definido por
def Surjective (f : α → β) : Prop := ∀ b, ∃ a, f a = b
Demostrar con Lean4 que si \(f\) es una función suprayectiva, entonces \(f\) tiene inversa por la derecha.
Para ello, completar la siguiente teoría de Lean4:
import Mathlib.Tactic open Function Classical variable {α β: Type _} variable {f : α → β} example (hf : Surjective f) : HasRightInverse f := by sorry