La equipotencia es una relación reflexiva
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 reflexiva.
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 |
import tactic open function def es_equipotente (A B : Type*) := ∃ g : A → B, bijective g infix ` ⋍ `: 50 := es_equipotente example : reflexive (⋍) := 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 |
import tactic open function def es_equipotente (A B : Type*) := ∃ g : A → B, bijective g infix ` ⋍ `: 50 := es_equipotente -- 1ª demostración example : reflexive (⋍) := begin intro X, use id, exact bijective_id, end -- 2ª demostración example : reflexive (⋍) := begin intro X, use [id, bijective_id], end -- 3ª demostración example : reflexive (⋍) := λ X, ⟨id, bijective_id⟩ -- 4ª demostración example : reflexive (⋍) := by tidy |
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 |
theory La_equipotencia_es_una_relacion_reflexiva imports Main "HOL-Library.Equipollence" begin (* 1ª demostración *) lemma "reflp (≈)" proof (rule reflpI) fix x :: "'a set" have "bij_betw id x x" by (simp only: bij_betw_id) then have "∃f. bij_betw f x x" by (simp only: exI) then show "x ≈ x" by (simp only: eqpoll_def) qed (* 2ª demostración *) lemma "reflp (≈)" by (simp only: reflpI eqpoll_refl) (* 3ª demostración *) lemma "reflp (≈)" by (simp add: reflpI) 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]
