Dos conjuntos A y B son equipotentes (y se denota por A \u2243 B) si existe una aplicaci\u00f3n biyectiva entre ellos. La equipotencia se puede definir en Lean por<\/p>\n
\n def es_equipotente (A B : Type*) :=\n \u2203 g : A \u2192 B, bijective g\n\n infix ` \u22cd `: 50 := es_equipotente\n<\/pre>\nDemostrar que la relaci\u00f3n de equipotencia es sim\u00e9trica.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport tactic\nopen function\n\ndef es_equipotente (A B : Type*) :=\n \u2203 g : A \u2192 B, bijective g\n\ninfix ` \u22cd `: 50 := es_equipotente\n\nvariables {X Y : Type*}\nvariable {f : X \u2192 Y}\nvariable {g : Y \u2192 X}\n\nexample : symmetric (\u22cd) :=\nsorry\n<\/pre>\n[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n
\r\nimport tactic\r\nopen function\r\n\r\ndef es_equipotente (A B : Type*) :=\r\n \u2203 g : A \u2192 B, bijective g\r\n\r\ninfix ` \u22cd `: 50 := es_equipotente\r\n\r\nvariables {X Y : Type*}\r\nvariable {f : X \u2192 Y}\r\nvariable {g : Y \u2192 X}\r\n\r\ndef inversa (f : X \u2192 Y) (g : Y \u2192 X) :=\r\n (\u2200 x, (g \u2218 f) x = x) \u2227 (\u2200 y, (f \u2218 g) y = y)\r\n\r\ndef tiene_inversa (f : X \u2192 Y) :=\r\n \u2203 g, inversa g f\r\n\r\nlemma aux1\r\n (hf : bijective f)\r\n : tiene_inversa f :=\r\nbegin\r\n cases (bijective_iff_has_inverse.mp hf) with g hg,\r\n by tidy,\r\nend\r\n\r\nlemma aux2\r\n (hf : bijective f)\r\n (hg : inversa g f)\r\n : bijective g :=\r\nbijective_iff_has_inverse.mpr (by use [f, hg])\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample : symmetric (\u22cd) :=\r\nbegin\r\n unfold symmetric,\r\n intros x y hxy,\r\n unfold es_equipotente at *,\r\n cases hxy with f hf,\r\n have h1 : tiene_inversa f := aux1 hf,\r\n cases h1 with g hg,\r\n use g,\r\n exact aux2 hf hg,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample : symmetric (\u22cd) :=\r\nbegin\r\n intros x y hxy,\r\n cases hxy with f hf,\r\n cases (aux1 hf) with g hg,\r\n use [g, aux2 hf hg],\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample : symmetric (\u22cd) :=\r\nbegin\r\n rintros x y \u27e8f, hf\u27e9,\r\n cases (aux1 hf) with g hg,\r\n use [g, aux2 hf hg],\r\nend\r\n<\/pre>\n