La equipotencia es una relación de equivalencia
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
|
1 2 3 4 |
def es_equipotente (A B : Type*) := ∃ g : A → B, bijective g infix ` ⋍ `: 50 := es_equipotente |
Demostrar que la relación de equipotencia es simétrica.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 |
import tactic open function def es_equipotente (A B : Type*) := ∃ g : A → B, bijective g infix ` ⋍ `: 50 := es_equipotente example : equivalence (⋍) := sorry |
[expand title=»Soluciones con Lean»]
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 |
import tactic open function def es_equipotente (A B : Type*) := ∃ g : A → B, bijective g infix ` ⋍ `: 50 := es_equipotente variables {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 := begin cases (bijective_iff_has_inverse.mp hf) with g hg, by tidy, end lemma aux2 (hf : bijective f) (hg : inversa g f) : bijective g := bijective_iff_has_inverse.mpr (by use [f, hg]) example : equivalence (⋍) := begin repeat {split}, { exact λ X, ⟨id, bijective_id⟩ }, { rintros X Y ⟨f, hf⟩, cases (aux1 hf) with g hg, use [g, aux2 hf hg], }, { rintros X Y Z ⟨f, hf⟩ ⟨g, hg⟩, exact ⟨g ∘ f, bijective.comp hg hf⟩, }, end |
Se puede interactuar con la prueba anterior en esta sesión con Lean.
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>
[/expand]
[expand title=»Soluciones con Isabelle/HOL»]
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 |
theory La_equipotencia_es_una_relacion_de_equivalencia imports Main "HOL-Library.Equipollence" begin (* 1ª demostración *) lemma "equivp (≈)" proof (rule equivpI) show "reflp (≈)" using reflpI eqpoll_refl by blast next show "symp (≈)" using sympI eqpoll_sym by blast next show "transp (≈)" using transpI eqpoll_trans by blast qed (* 2ª demostración *) lemma "equivp (≈)" by (simp add: equivp_reflp_symp_transp reflpI sympI eqpoll_sym transpI eqpoll_trans) end |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]
