{"id":8186,"date":"2024-05-04T11:48:28","date_gmt":"2024-05-04T09:48:28","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=8186"},"modified":"2024-05-04T11:52:51","modified_gmt":"2024-05-04T09:52:51","slug":"04-may-24-b","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/04-may-24-b\/","title":{"rendered":"La semana en Calculemus (4 de mayo de 2024)"},"content":{"rendered":"\n<p>Esta semana he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. Imagen de la interseccion general mediante aplicaciones inyectivas<\/a><\/li>\n<li><a href=\"#ej2\">2. Imagen inversa de la uni\u00f3n general<\/a><\/li>\n<li><a href=\"#ej3\">3. Imagen inversa de la intersecci\u00f3n general<\/a><\/li>\n<li><a href=\"#ej4\">4. Teorema de Cantor<\/a><\/li>\n<li><a href=\"#ej5\">5. En los monoides, los inversos a la izquierda y a la derecha son iguales<\/a><\/li>\n<\/ul>\n<p>A continuaci\u00f3n se muestran las soluciones.<br \/>\n<!--more--><br \/>\n<a name=\"ej1\"><\/a><\/p>\n<h3>1. Imagen de la interseccion general mediante aplicaciones inyectivas<\/h3>\n<p>Demostrar con Lean4 que si &#92;(f&#92;) es inyectiva, entonces<br \/>\n&#92;[\u22c2\u1d62f[A\u1d62] \u2286 f\\left[\u22c2\u1d62A\u1d62\\right] &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set Function\n\nvariable {\u03b1 \u03b2 I : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (A : I \u2192 Set \u03b1)\n\nexample\n  (i : I)\n  (injf : Injective f)\n  : (\u22c2 i, f '' A i) \u2286 f '' (\u22c2 i, A i) :=\nby\nsorry\n<\/pre>\n<h4>1.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Sea &#92;(y \u2208 \u22c2\u1d62f[A\u1d62]&#92;). Entonces,<br \/>\n&#92;begin{align}<br \/>\n   &amp; (\u2200i \u2208 I)y \u2208 f[A\u1d62]  &#92;tag{1} &#92;&#92;<br \/>\n   &amp; y \u2208 f[A\u1d62]<br \/>\n&#92;end{align}<br \/>\nPor tanto, existe un &#92;(x \u2208 A\u1d62&#92;) tal que<br \/>\n&#92;[ f(x) = y &#92;tag{2} &#92;]<\/p>\n<p>Veamos que &#92;(x \u2208 \u22c2\u1d62A\u1d62&#92;). Para ello, sea &#92;(j \u2208 I&#92;). Por (1),<br \/>\n&#92;[ y \u2208 f[A\u2c7c] &#92;]<br \/>\nLuego, existe un &#92;(z&#92;) tal que<br \/>\n&#92;begin{align}<br \/>\n   &amp;z \u2208 A\u2c7c    &#92;tag{3} &#92;&#92;<br \/>\n   &amp;f(z) = y<br \/>\n&#92;end{align}<br \/>\nPot (2),<br \/>\n&#92;[ f(x) = f(z) &#92;]<br \/>\ny, por ser &#92;(f&#92;) inyectiva,<br \/>\n&#92;[ x = z &#92;]<br \/>\ny, por (3),<br \/>\n&#92;[ x \u2208 A\u2c7c &#92;]<\/p>\n<p>Puesto que &#92;(x \u2208 \u22c2\u1d62A\u1d62&#92;) se tiene que &#92;(f(x) \u2208 f\\left[\u22c2\u1d62A\u1d62\\right]&#92;) y, por (2), &#92;(y \u2208 f\\left[\u22c2\u1d62A\u1d62\\right]&#92;).<\/p>\n<h4>1.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set Function\n\nvariable {\u03b1 \u03b2 I : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (A : I \u2192 Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (i : I)\n  (injf : Injective f)\n  : (\u22c2 i, f '' A i) \u2286 f '' (\u22c2 i, A i) :=\nby\n  intros y hy\n  -- y : \u03b2\n  -- hy : y \u2208 \u22c2 (i : I), f '' A i\n  -- \u22a2 y \u2208 f '' \u22c2 (i : I), A i\n  have h1 : \u2200 (i : I), y \u2208 f '' A i := mem_iInter.mp hy\n  have h2 : y \u2208 f '' A i := h1 i\n  obtain \u27e8x : \u03b1, h3 : x \u2208 A i \u2227 f x = y\u27e9 := h2\n  have h4 : f x = y := h3.2\n  have h5 : \u2200 i : I, x \u2208 A i := by\n    intro j\n    have h5a : y \u2208 f '' A j := h1 j\n    obtain \u27e8z : \u03b1, h5b : z \u2208 A j \u2227 f z = y\u27e9 := h5a\n    have h5c : z \u2208 A j := h5b.1\n    have h5d : f z = y := h5b.2\n    have h5e : f z = f x := by rwa [\u2190h4] at h5d\n    have h5f : z = x := injf h5e\n    show x \u2208 A j\n    rwa [h5f] at h5c\n  have h6 : x \u2208 \u22c2 i, A i := mem_iInter.mpr h5\n  have h7 : f x \u2208 f '' (\u22c2 i, A i) := mem_image_of_mem f h6\n  show y \u2208 f '' (\u22c2 i, A i)\n  rwa [h4] at h7\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (i : I)\n  (injf : Injective f)\n  : (\u22c2 i, f '' A i) \u2286 f '' (\u22c2 i, A i) :=\nby\n  intros y hy\n  -- y : \u03b2\n  -- hy : y \u2208 \u22c2 (i : I), f '' A i\n  -- \u22a2 y \u2208 f '' \u22c2 (i : I), A i\n  rw [mem_iInter] at hy\n  -- hy : \u2200 (i : I), y \u2208 f '' A i\n  rcases hy i with \u27e8x, -, fxy\u27e9\n  -- x : \u03b1\n  -- fxy : f x = y\n  use x\n  -- \u22a2 x \u2208 \u22c2 (i : I), A i \u2227 f x = y\n  constructor\n  . -- \u22a2 x \u2208 \u22c2 (i : I), A i\n    apply mem_iInter_of_mem\n    -- \u22a2 \u2200 (i : I), x \u2208 A i\n    intro j\n    -- j : I\n    -- \u22a2 x \u2208 A j\n    rcases hy j with \u27e8z, zAj, fzy\u27e9\n    -- z : \u03b1\n    -- zAj : z \u2208 A j\n    -- fzy : f z = y\n    convert zAj\n    -- \u22a2 x = z\n    apply injf\n    -- \u22a2 f x = f z\n    rw [fxy]\n    -- \u22a2 y = f z\n    rw [\u2190fzy]\n  . -- \u22a2 f x = y\n    exact fxy\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (i : I)\n  (injf : Injective f)\n  : (\u22c2 i, f '' A i) \u2286 f '' (\u22c2 i, A i) :=\nby\n  intro y\n  -- y : \u03b2\n  -- \u22a2 y \u2208 \u22c2 (i : I), f '' A i \u2192 y \u2208 f '' \u22c2 (i : I), A i\n  simp\n  -- \u22a2 (\u2200 (i : I), \u2203 x, x \u2208 A i \u2227 f x = y) \u2192 \u2203 x, (\u2200 (i : I), x \u2208 A i) \u2227 f x = y\n  intro h\n  -- h : \u2200 (i : I), \u2203 x, x \u2208 A i \u2227 f x = y\n  -- \u22a2 \u2203 x, (\u2200 (i : I), x \u2208 A i) \u2227 f x = y\n  rcases h i with \u27e8x, -, fxy\u27e9\n  -- x : \u03b1\n  -- fxy : f x = y\n  use x\n  -- \u22a2 (\u2200 (i : I), x \u2208 A i) \u2227 f x = y\n  constructor\n  . -- \u22a2 \u2200 (i : I), x \u2208 A i\n    intro j\n    -- j : I\n    -- \u22a2 x \u2208 A j\n    rcases h j with \u27e8z, zAi, fzy\u27e9\n    -- z : \u03b1\n    -- zAi : z \u2208 A j\n    -- fzy : f z = y\n    have : f x = f z := by rw [fxy, fzy]\n    -- this : f x = f z\n    have : x = z := injf this\n    -- this : x = z\n    rw [this]\n    -- \u22a2 z \u2208 A j\n    exact zAi\n  . -- \u22a2 f x = y\n    exact fxy\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (s : Set \u03b1)\n-- #check (mem_iInter : x \u2208 \u22c2 i, A i \u2194 \u2200 i, x \u2208 A i)\n-- #check (mem_iInter_of_mem : (\u2200 i, x \u2208 A i) \u2192 x \u2208 \u22c2 i, A i)\n-- #check (mem_image_of_mem f : x  \u2208 s \u2192 f x \u2208 f '' s)\n<\/pre>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Imagen_de_la_interseccion_general_mediante_inyectiva.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>1.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Imagen_de_la_interseccion_general_mediante_inyectiva\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"i \u2208 I\"\n          \"inj f\"\n  shows \"(\u22c2 i \u2208 I. f ` A i) \u2286 f ` (\u22c2 i \u2208 I. A i)\"\nproof (rule subsetI)\n  fix y\n  assume \"y \u2208 (\u22c2 i \u2208 I. f ` A i)\"\n  then have \"y \u2208 f ` A i\"\n    using \u2039i \u2208 I\u203a by (rule INT_D)\n  then show \"y \u2208 f ` (\u22c2 i \u2208 I. A i)\"\n  proof (rule imageE)\n    fix x\n    assume \"y = f x\"\n    assume \"x \u2208 A i\"\n    have \"x \u2208 (\u22c2 i \u2208 I. A i)\"\n    proof (rule INT_I)\n      fix j\n      assume \"j \u2208 I\"\n      show \"x \u2208 A j\"\n      proof -\n        have \"y \u2208 f ` A j\"\n          using \u2039y \u2208 (\u22c2i\u2208I. f ` A i)\u203a \u2039j \u2208 I\u203a by (rule INT_D)\n        then show \"x \u2208 A j\"\n        proof (rule imageE)\n          fix z\n          assume \"y = f z\"\n          assume \"z \u2208 A j\"\n          have \"f z = f x\"\n            using \u2039y = f z\u203a \u2039y = f x\u203a by (rule subst)\n          with \u2039inj f\u203a have \"z = x\"\n            by (rule injD)\n          then show \"x \u2208 A j\"\n            using \u2039z \u2208 A j\u203a by (rule subst)\n        qed\n      qed\n    qed\n    then have \"f x \u2208 f ` (\u22c2 i \u2208 I. A i)\"\n      by (rule imageI)\n    with \u2039y = f x\u203a show \"y \u2208 f ` (\u22c2 i \u2208 I. A i)\"\n      by (rule ssubst)\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"i \u2208 I\"\n          \"inj f\"\n  shows \"(\u22c2 i \u2208 I. f ` A i) \u2286 f ` (\u22c2 i \u2208 I. A i)\"\nproof\n  fix y\n  assume \"y \u2208 (\u22c2 i \u2208 I. f ` A i)\"\n  then have \"y \u2208 f ` A i\" using \u2039i \u2208 I\u203a by simp\n  then show \"y \u2208 f ` (\u22c2 i \u2208 I. A i)\"\n  proof\n    fix x\n    assume \"y = f x\"\n    assume \"x \u2208 A i\"\n    have \"x \u2208 (\u22c2 i \u2208 I. A i)\"\n    proof\n      fix j\n      assume \"j \u2208 I\"\n      show \"x \u2208 A j\"\n      proof -\n        have \"y \u2208 f ` A j\"\n          using \u2039y \u2208 (\u22c2i\u2208I. f ` A i)\u203a \u2039j \u2208 I\u203a by simp\n        then show \"x \u2208 A j\"\n        proof\n          fix z\n          assume \"y = f z\"\n          assume \"z \u2208 A j\"\n          have \"f z = f x\" using \u2039y = f z\u203a \u2039y = f x\u203a by simp\n          with \u2039inj f\u203a have \"z = x\" by (rule injD)\n          then show \"x \u2208 A j\" using \u2039z \u2208 A j\u203a by simp\n        qed\n      qed\n    qed\n    then have \"f x \u2208 f ` (\u22c2 i \u2208 I. A i)\" by simp\n    with \u2039y = f x\u203a show \"y \u2208 f ` (\u22c2 i \u2208 I. A i)\" by simp\n  qed\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"i \u2208 I\"\n          \"inj f\"\n  shows \"(\u22c2 i \u2208 I. f ` A i) \u2286 f ` (\u22c2 i \u2208 I. A i)\"\n  using assms\n  by (simp add: image_INT)\n\nend\n<\/pre>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. Imagen inversa de la uni\u00f3n general<\/h3>\n<p>Demostrar con Lean4 que<br \/>\n&#92;[ f\u207b\u00b9&#92;left[\u22c3\u1d62 B\u1d62&#92;right] = \u22c3\u1d62 f\u207b\u00b9[B\u1d62] &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 \u03b2 I : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (B : I \u2192 Set \u03b2)\n\nexample : f \u207b\u00b9' (\u22c3 i, B i) = \u22c3 i, f \u207b\u00b9' (B i) :=\nby sorry\n<\/pre>\n<h4>2.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Tenemos que demostrar que, para todo &#92;(x&#92;),<br \/>\n&#92;[ x \u2208 f\u207b\u00b9&#92;left[\u22c3\u1d62 B\u1d62&#92;right] \u2194 x \u2208 \u22c3\u1d62 f\u207b\u00b9[B\u1d62] &#92;]<br \/>\ny lo haremos demostrando las dos implicaciones.<\/p>\n<p>(\u27f9) Supongamos que &#92;(x \u2208 f\u207b\u00b9&#92;left[\u22c3\u1d62 B\u1d62&#92;right]&#92;). Entonces, por la definici\u00f3n de la imagen inversa,<br \/>\n&#92;[ f(x) \u2208 \u22c3\u1d62 B\u1d62 &#92;]<br \/>\ny, por la definici\u00f3n de la uni\u00f3n, existe un &#92;(i&#92;) tal que<br \/>\n&#92;[ f(x) \u2208 B\u1d62 &#92;]<br \/>\ny, por la definici\u00f3n de la imagen inversa,<br \/>\n&#92;[ x \u2208 f\u207b\u00b9[B\u1d62] &#92;]<br \/>\ny, por la definici\u00f3n de la uni\u00f3n,<br \/>\n&#92;[ x \u2208 \u22c3\u1d62 f\u207b\u00b9[B\u1d62] &#92;]<\/p>\n<p>(\u27f8) Supongamos que &#92;(x \u2208 \u22c3\u1d62 f\u207b\u00b9[B\u1d62]&#92;). Entonces, por la definici\u00f3n de la uni\u00f3n, existe un &#92;(i&#92;) tal que<br \/>\n&#92;[ x \u2208 f\u207b\u00b9[B\u1d62] &#92;]<br \/>\ny, por la definici\u00f3n de la imagen inversa,<br \/>\n&#92;[ f(x) \u2208 B\u1d62 &#92;]<br \/>\ny, por la definici\u00f3n de la uni\u00f3n,<br \/>\n&#92;[ f(x) \u2208 \u22c3\u1d62 B\u1d62 &#92;]<br \/>\ny, por la definici\u00f3n de la imagen inversa,<br \/>\n&#92;[ x \u2208 f\u207b\u00b9&#92;left[\u22c3\u1d62 B\u1d62&#92;right] &#92;]<\/p>\n<h4>2.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 \u03b2 I : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (B : I \u2192 Set \u03b2)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c3 i, B i) = \u22c3 i, f \u207b\u00b9' (B i) :=\nby\n  ext x\n  -- x : \u03b1\n  -- \u22a2 x \u2208 f \u207b\u00b9' \u22c3 (i : I), B i \u2194 x \u2208 \u22c3 (i : I), f \u207b\u00b9' B i\n  constructor\n  . -- \u22a2 x \u2208 f \u207b\u00b9' \u22c3 (i : I), B i \u2192 x \u2208 \u22c3 (i : I), f \u207b\u00b9' B i\n    intro hx\n    -- hx : x \u2208 f \u207b\u00b9' \u22c3 (i : I), B i\n    -- \u22a2 x \u2208 \u22c3 (i : I), f \u207b\u00b9' B i\n    rw [mem_preimage] at hx\n    -- hx : f x \u2208 \u22c3 (i : I), B i\n    rw [mem_iUnion] at hx\n    -- hx : \u2203 i, f x \u2208 B i\n    cases' hx with i fxBi\n    -- i : I\n    -- fxBi : f x \u2208 B i\n    rw [mem_iUnion]\n    -- \u22a2 \u2203 i, x \u2208 f \u207b\u00b9' B i\n    use i\n    -- \u22a2 x \u2208 f \u207b\u00b9' B i\n    apply mem_preimage.mpr\n    -- \u22a2 f x \u2208 B i\n    exact fxBi\n  . -- \u22a2 x \u2208 \u22c3 (i : I), f \u207b\u00b9' B i \u2192 x \u2208 f \u207b\u00b9' \u22c3 (i : I), B i\n    intro hx\n    -- hx : x \u2208 \u22c3 (i : I), f \u207b\u00b9' B i\n    -- \u22a2 x \u2208 f \u207b\u00b9' \u22c3 (i : I), B i\n    rw [mem_preimage]\n    -- \u22a2 f x \u2208 \u22c3 (i : I), B i\n    rw [mem_iUnion]\n    -- \u22a2 \u2203 i, f x \u2208 B i\n    rw [mem_iUnion] at hx\n    -- hx : \u2203 i, x \u2208 f \u207b\u00b9' B i\n    cases' hx with i xBi\n    -- i : I\n    -- xBi : x \u2208 f \u207b\u00b9' B i\n    use i\n    -- \u22a2 f x \u2208 B i\n    rw [mem_preimage] at xBi\n    -- xBi : f x \u2208 B i\n    exact xBi\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c3 i, B i) = \u22c3 i, f \u207b\u00b9' (B i) :=\npreimage_iUnion\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c3 i, B i) = \u22c3 i, f \u207b\u00b9' (B i) :=\nby  simp\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (s : Set \u03b2)\n-- variable (A : I \u2192 Set \u03b1)\n-- #check (mem_iUnion : x \u2208 \u22c3 i, A i \u2194 \u2203 i, x \u2208 A i)\n-- #check (mem_preimage : x \u2208 f \u207b\u00b9' s \u2194 f x \u2208 s)\n-- #check (preimage_iUnion : f \u207b\u00b9' (\u22c3 i, B i) = \u22c3 i, f \u207b\u00b9' (B i))\n<\/pre>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Imagen_inversa_de_la_union_general.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>2.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Imagen_inversa_de_la_union_general\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma \"f -` (\u22c3 i \u2208 I. B i) = (\u22c3 i \u2208 I. f -` B i)\"\nproof (rule equalityI)\n  show \"f -` (\u22c3 i \u2208 I. B i) \u2286 (\u22c3 i \u2208 I. f -` B i)\"\n  proof (rule subsetI)\n    fix x\n    assume \"x \u2208 f -` (\u22c3 i \u2208 I. B i)\"\n    then have \"f x \u2208 (\u22c3 i \u2208 I. B i)\"\n      by (rule vimageD)\n    then show \"x \u2208 (\u22c3 i \u2208 I. f -` B i)\"\n    proof (rule UN_E)\n      fix i\n      assume \"i \u2208 I\"\n      assume \"f x \u2208 B i\"\n      then have \"x \u2208 f -` B i\"\n        by (rule vimageI2)\n      with \u2039i \u2208 I\u203a show \"x \u2208 (\u22c3 i \u2208 I. f -` B i)\"\n        by (rule UN_I)\n    qed\n  qed\nnext\n  show \"(\u22c3 i \u2208 I. f -` B i) \u2286 f -` (\u22c3 i \u2208 I. B i)\"\n  proof (rule subsetI)\n    fix x\n    assume \"x \u2208 (\u22c3 i \u2208 I. f -` B i)\"\n    then show \"x \u2208 f -` (\u22c3 i \u2208 I. B i)\"\n    proof (rule UN_E)\n      fix i\n      assume \"i \u2208 I\"\n      assume \"x \u2208 f -` B i\"\n      then have \"f x \u2208 B i\"\n        by (rule vimageD)\n      with \u2039i \u2208 I\u203a have \"f x \u2208 (\u22c3 i \u2208 I. B i)\"\n        by (rule UN_I)\n      then show \"x \u2208 f -` (\u22c3 i \u2208 I. B i)\"\n        by (rule vimageI2)\n    qed\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma \"f -` (\u22c3 i \u2208 I. B i) = (\u22c3 i \u2208 I. f -` B i)\"\nproof\n  show \"f -` (\u22c3 i \u2208 I. B i) \u2286 (\u22c3 i \u2208 I. f -` B i)\"\n  proof\n    fix x\n    assume \"x \u2208 f -` (\u22c3 i \u2208 I. B i)\"\n    then have \"f x \u2208 (\u22c3 i \u2208 I. B i)\" by simp\n    then show \"x \u2208 (\u22c3 i \u2208 I. f -` B i)\"\n    proof\n      fix i\n      assume \"i \u2208 I\"\n      assume \"f x \u2208 B i\"\n      then have \"x \u2208 f -` B i\" by simp\n      with \u2039i \u2208 I\u203a show \"x \u2208 (\u22c3 i \u2208 I. f -` B i)\" by (rule UN_I)\n    qed\n  qed\nnext\n  show \"(\u22c3 i \u2208 I. f -` B i) \u2286 f -` (\u22c3 i \u2208 I. B i)\"\n  proof\n    fix x\n    assume \"x \u2208 (\u22c3 i \u2208 I. f -` B i)\"\n    then show \"x \u2208 f -` (\u22c3 i \u2208 I. B i)\"\n    proof\n      fix i\n      assume \"i \u2208 I\"\n      assume \"x \u2208 f -` B i\"\n      then have \"f x \u2208 B i\" by simp\n      with \u2039i \u2208 I\u203a have \"f x \u2208 (\u22c3 i \u2208 I. B i)\" by (rule UN_I)\n      then show \"x \u2208 f -` (\u22c3 i \u2208 I. B i)\" by simp\n    qed\n  qed\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma \"f -` (\u22c3 i \u2208 I. B i) = (\u22c3 i \u2208 I. f -` B i)\"\n  by (simp only: vimage_UN)\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma \"f -` (\u22c3 i \u2208 I. B i) = (\u22c3 i \u2208 I. f -` B i)\"\n  by auto\n\nend\n<\/pre>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. Imagen inversa de la intersecci\u00f3n general<\/h3>\n<p>Demostrar con Lean4 que<br \/>\n&#92;[ f\u207b\u00b9&#92;left[&#92;bigcap_{i &#92;in I} B_i&#92;right] = &#92;bigcap_{i &#92;in I} f\u207b\u00b9[B_i] &#92;]<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 \u03b2 I : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (B : I \u2192 Set \u03b2)\n\nexample : f \u207b\u00b9' (\u22c2 i, B i) = \u22c2 i, f \u207b\u00b9' (B i) :=\nby sorry\n<\/pre>\n<h4>3.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Se demuestra mediante la siguiente cadena de equivalencias<br \/>\n&#92;begin{align}<br \/>\n   x \u2208 f\u207b\u00b9&#92;left[&#92;bigcap_{i &#92;in I} B_i&#92;right]<br \/>\n   &amp;\u2194 f(x) \u2208 &#92;bigcap_{i &#92;in I} B_i            &#92;&#92;<br \/>\n   &amp;\u2194 (\u2200 i) f(x) \u2208 B_i                       &#92;&#92;<br \/>\n   &amp;\u2194 (\u2200 i) x \u2208 f\u207b\u00b9[B_i]                     &#92;&#92;<br \/>\n   &amp;\u2194 x \u2208 &#92;bigcap_{i &#92;in I} f\u207b\u00b9[B_i]<br \/>\n&#92;end{align}<\/p>\n<h4>3.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 \u03b2 I : Type _}\nvariable (f : \u03b1 \u2192 \u03b2)\nvariable (B : I \u2192 Set \u03b2)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c2 i, B i) = \u22c2 i, f \u207b\u00b9' (B i) :=\nby\n  ext x\n  -- x : \u03b1\n  -- \u22a2 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i \u2194 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n  calc  (x \u2208 f \u207b\u00b9' \u22c2 i, B i)\n     \u2194 f x \u2208 \u22c2 i, B i       := mem_preimage\n   _ \u2194 (\u2200 i, f x \u2208 B i)     := mem_iInter\n   _ \u2194 (\u2200 i, x \u2208 f \u207b\u00b9' B i) := iff_of_eq rfl\n   _ \u2194 x \u2208 \u22c2 i, f \u207b\u00b9' B i   := mem_iInter.symm\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c2 i, B i) = \u22c2 i, f \u207b\u00b9' (B i) :=\nby\n  ext x\n  -- x : \u03b1\n  -- \u22a2 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i \u2194 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n  constructor\n  . -- \u22a2 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i \u2192 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n    intro hx\n    -- hx : x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i\n    -- \u22a2 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n    apply mem_iInter_of_mem\n    -- \u22a2 \u2200 (i : I), x \u2208 f \u207b\u00b9' B i\n    intro i\n    -- i : I\n    -- \u22a2 x \u2208 f \u207b\u00b9' B i\n    rw [mem_preimage]\n    -- \u22a2 f x \u2208 B i\n    rw [mem_preimage] at hx\n    -- hx : f x \u2208 \u22c2 (i : I), B i\n    rw [mem_iInter] at hx\n    -- hx : \u2200 (i : I), f x \u2208 B i\n    exact hx i\n  . -- \u22a2 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i \u2192 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i\n    intro hx\n    -- hx : x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n    -- \u22a2 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i\n    rw [mem_preimage]\n    -- \u22a2 f x \u2208 \u22c2 (i : I), B i\n    rw [mem_iInter]\n    -- \u22a2 \u2200 (i : I), f x \u2208 B i\n    intro i\n    -- i : I\n    -- \u22a2 f x \u2208 B i\n    rw [\u2190mem_preimage]\n    -- \u22a2 x \u2208 f \u207b\u00b9' B i\n    rw [mem_iInter] at hx\n    -- hx : \u2200 (i : I), x \u2208 f \u207b\u00b9' B i\n    exact hx i\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c2 i, B i) = \u22c2 i, f \u207b\u00b9' (B i) :=\nby\n  ext x\n  -- \u22a2 x \u2208 f \u207b\u00b9' \u22c2 (i : I), B i \u2194 x \u2208 \u22c2 (i : I), f \u207b\u00b9' B i\n  simp\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : f \u207b\u00b9' (\u22c2 i, B i) = \u22c2 i, f \u207b\u00b9' (B i) :=\nby { ext ; simp }\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (s : Set \u03b2)\n-- variable (A : I \u2192 Set \u03b1)\n-- variable (a b : Prop)\n-- #check (iff_of_eq : a = b \u2192 (a \u2194 b))\n-- #check (mem_iInter : x \u2208 \u22c2 i, A i \u2194 \u2200 i, x \u2208 A i)\n-- #check (mem_iInter_of_mem : (\u2200 i, x \u2208 A i) \u2192 x \u2208 \u22c2 i, A i)\n-- #check (mem_preimage : x \u2208 f \u207b\u00b9' s \u2194 f x \u2208 s)\n<\/pre>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Imagen_inversa_de_la_interseccion_general.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>3.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Imagen_inversa_de_la_interseccion_general\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma \"f -` (\u22c2 i \u2208 I. B i) = (\u22c2 i \u2208 I. f -` B i)\"\nproof (rule equalityI)\n  show \"f -` (\u22c2 i \u2208 I. B i) \u2286 (\u22c2 i \u2208 I. f -` B i)\"\n  proof (rule subsetI)\n    fix x\n    assume \"x \u2208 f -` (\u22c2 i \u2208 I. B i)\"\n    show \"x \u2208 (\u22c2 i \u2208 I. f -` B i)\"\n    proof (rule INT_I)\n      fix i\n      assume \"i \u2208 I\"\n      have \"f x \u2208 (\u22c2 i \u2208 I. B i)\"\n        using \u2039x \u2208 f -` (\u22c2 i \u2208 I. B i)\u203a by (rule vimageD)\n      then have \"f x \u2208 B i\"\n        using \u2039i \u2208 I\u203a by (rule INT_D)\n      then show \"x \u2208 f -` B i\"\n        by (rule vimageI2)\n    qed\n  qed\nnext\n  show \"(\u22c2 i \u2208 I. f -` B i) \u2286 f -` (\u22c2 i \u2208 I. B i)\"\n  proof (rule subsetI)\n    fix x\n    assume \"x \u2208 (\u22c2 i \u2208 I. f -` B i)\"\n    have \"f x \u2208 (\u22c2 i \u2208 I. B i)\"\n    proof (rule INT_I)\n      fix i\n      assume \"i \u2208 I\"\n      with \u2039x \u2208 (\u22c2 i \u2208 I. f -` B i)\u203a have \"x \u2208 f -` B i\"\n        by (rule INT_D)\n      then show \"f x \u2208 B i\"\n        by (rule vimageD)\n    qed\n    then show \"x \u2208 f -` (\u22c2 i \u2208 I. B i)\"\n      by (rule vimageI2)\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma \"f -` (\u22c2 i \u2208 I. B i) = (\u22c2 i \u2208 I. f -` B i)\"\nproof\n  show \"f -` (\u22c2 i \u2208 I. B i) \u2286 (\u22c2 i \u2208 I. f -` B i)\"\n  proof (rule subsetI)\n    fix x\n    assume hx : \"x \u2208 f -` (\u22c2 i \u2208 I. B i)\"\n    show \"x \u2208 (\u22c2 i \u2208 I. f -` B i)\"\n    proof\n      fix i\n      assume \"i \u2208 I\"\n      have \"f x \u2208 (\u22c2 i \u2208 I. B i)\" using hx by simp\n      then have \"f x \u2208 B i\" using \u2039i \u2208 I\u203a by simp\n      then show \"x \u2208 f -` B i\" by simp\n    qed\n  qed\nnext\n  show \"(\u22c2 i \u2208 I. f -` B i) \u2286 f -` (\u22c2 i \u2208 I. B i)\"\n  proof\n    fix x\n    assume \"x \u2208 (\u22c2 i \u2208 I. f -` B i)\"\n    have \"f x \u2208 (\u22c2 i \u2208 I. B i)\"\n    proof\n      fix i\n      assume \"i \u2208 I\"\n      with \u2039x \u2208 (\u22c2 i \u2208 I. f -` B i)\u203a have \"x \u2208 f -` B i\" by simp\n      then show \"f x \u2208 B i\" by simp\n    qed\n    then show \"x \u2208 f -` (\u22c2 i \u2208 I. B i)\" by simp\n  qed\nqed\n\n(* 3 demostraci\u00f3n *)\n\nlemma \"f -` (\u22c2 i \u2208 I. B i) = (\u22c2 i \u2208 I. f -` B i)\"\n  by (simp only: vimage_INT)\n\n(* 4\u00aa demostraci\u00f3n *)\n\nlemma \"f -` (\u22c2 i \u2208 I. B i) = (\u22c2 i \u2208 I. f -` B i)\"\n  by auto\n\nend\n<\/pre>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. Teorema de Cantor<\/h3>\n<p>Demostrar con Lean4 el teorema de Cantor; es decir, que no existe ninguna aplicaci\u00f3n suprayectiva de un conjunto en el conjunto de sus subconjuntos.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nopen Function\n\nvariable {\u03b1 : Type}\n\nexample : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00acSurjective f :=\nby sorry\n<\/pre>\n<h4>4.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Sea &#92;(f&#92;) una funci\u00f3n de &#92;(A&#92;) en el conjunto de los subconjuntos  &#92;(A&#92;). Tenemos que demostrar que &#92;(f&#92;) no es suprayectiva. Lo haremos por reducci\u00f3n al absurdo. Para ello, supongamos que &#92;(f&#92;) es suprayectiva y consideremos el conjunto<br \/>\n&#92;[ S := &#92;{i \u2208 A | i \u2209 f(i)&#92;} &#92;tag{1} &#92;]<br \/>\nEntonces, tiene que existir un &#92;(j \u2208 A&#92;) tal que<br \/>\n&#92;[ f(j) = S &#92;tag{2} &#92;]<br \/>\nSe pueden dar dos casos: &#92;(j \u2208 S&#92;) \u00f3 &#92;(j \u2209 S&#92;). Veamos que ambos son imposibles.<\/p>\n<p>Caso 1: Supongamos que &#92;(j \u2208 S&#92;). Entonces, por (1)<br \/>\n&#92;[ j \u2209 f(j) &#92;]<br \/>\ny, por (2),<br \/>\n&#92;[ j \u2209 S &#92;]<br \/>\nque es una contradicci\u00f3n.<\/p>\n<p>Caso 2: Supongamos que &#92;(j \u2209 S&#92;). Entonces, por (1)<br \/>\n&#92;[ j \u2208 f(j) &#92;]<br \/>\ny, por (2),<br \/>\n&#92;[ j \u2208 S &#92;]<br \/>\nque es una contradicci\u00f3n.<\/p>\n<h4>4.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Data.Set.Basic\nopen Function\n\nvariable {\u03b1 : Type}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00acSurjective f :=\nby\n  intros f hf\n  -- f : \u03b1 \u2192 Set \u03b1\n  -- hf : Surjective f\n  -- \u22a2 False\n  let S := {i | i \u2209 f i}\n  unfold Surjective at hf\n  -- hf : \u2200 (b : Set \u03b1), \u2203 a, f a = b\n  cases' hf S with j hj\n  -- j : \u03b1\n  -- hj : f j = S\n  by_cases j \u2208 S\n  . -- h : j \u2208 S\n    dsimp at h\n    -- h : \u00acj \u2208 f j\n    apply h\n    -- \u22a2 j \u2208 f j\n    rw [hj]\n    -- \u22a2 j \u2208 S\n    exact h\n  . -- h : \u00acj \u2208 S\n    apply h\n    -- \u22a2 j \u2208 S\n    rw [\u2190hj] at h\n    -- h : \u00acj \u2208 f j\n    exact h\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00ac Surjective f :=\nby\n  intros f hf\n  -- f : \u03b1 \u2192 Set \u03b1\n  -- hf : Surjective f\n  -- \u22a2 False\n  let S := {i | i \u2209 f i}\n  cases' hf S with j hj\n  -- j : \u03b1\n  -- hj : f j = S\n  by_cases j \u2208 S\n  . -- h : j \u2208 S\n    apply h\n    -- \u22a2 j \u2208 f j\n    rwa [hj]\n  . -- h : \u00acj \u2208 S\n    apply h\n    rwa [\u2190hj] at h\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00ac Surjective f :=\nby\n  intros f hf\n  -- f : \u03b1 \u2192 Set \u03b1\n  -- hf : Surjective f\n  -- \u22a2 False\n  let S := {i | i \u2209 f i}\n  cases' hf S with j hj\n  -- j : \u03b1\n  -- hj : f j = S\n  have h : (j \u2208 S) = (j \u2209 S) :=\n    calc  (j \u2208 S)\n       = (j \u2209 f j) := Set.mem_setOf_eq\n     _ = (j \u2209 S)   := congrArg (j \u2209 .) hj\n  exact iff_not_self (iff_of_eq h)\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00ac Surjective f :=\ncantor_surjective\n\n-- Lemas usados\n-- ============\n\n-- variable (x : \u03b1)\n-- variable (p : \u03b1 \u2192 Prop)\n-- variable (a b : Prop)\n-- #check (Set.mem_setOf_eq : (x \u2208 {y : \u03b1 | p y}) = p x)\n-- #check (iff_of_eq : a = b \u2192 (a \u2194 b))\n-- #check (iff_not_self : \u00ac(a \u2194 \u00aca))\n-- #check (cantor_surjective : \u2200 f : \u03b1 \u2192 Set \u03b1, \u00ac Surjective f)\n<\/pre>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/Teorema_de_Cantor.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>4.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory Teorema_de_Cantor\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\ntheorem\n  fixes f :: \"'\u03b1 \u21d2 '\u03b1 set\"\n  shows \"\u00ac surj f\"\nproof (rule notI)\n  assume \"surj f\"\n  let ?S = \"{i. i \u2209 f i}\"\n  have \"\u2203 j. ?S = f j\"\n    using \u2039surj f\u203a by (simp only: surjD)\n  then obtain j where \"?S = f j\"\n    by (rule exE)\n  show False\n  proof (cases \"j \u2208 ?S\")\n    assume \"j \u2208 ?S\"\n    then have \"j \u2209 f j\"\n      by (rule CollectD)\n    moreover\n    have \"j \u2208 f j\"\n      using \u2039?S = f j\u203a \u2039j \u2208 ?S\u203a by (rule subst)\n    ultimately show False\n      by (rule notE)\n  next\n    assume \"j \u2209 ?S\"\n    with \u2039?S = f j\u203a have \"j \u2209 f j\"\n      by (rule subst)\n    then have \"j \u2208 ?S\"\n      by (rule CollectI)\n    with \u2039j \u2209 ?S\u203a show False\n      by (rule notE)\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\ntheorem\n  fixes f :: \"'\u03b1 \u21d2 '\u03b1 set\"\n  shows \"\u00ac surj f\"\nproof (rule notI)\n  assume \"surj f\"\n  let ?S = \"{i. i \u2209 f i}\"\n  have \"\u2203 j. ?S = f j\"\n    using \u2039surj f\u203a by (simp only: surjD)\n  then obtain j where \"?S = f j\"\n    by (rule exE)\n  have \"j \u2209 ?S\"\n  proof (rule notI)\n    assume \"j \u2208 ?S\"\n    then have \"j \u2209 f j\"\n      by (rule CollectD)\n    with \u2039?S = f j\u203a have \"j \u2209 ?S\"\n      by (rule ssubst)\n    then show False\n      using \u2039j \u2208 ?S\u203a by (rule notE)\n  qed\n  moreover\n  have \"j \u2208 ?S\"\n  proof (rule CollectI)\n    show \"j \u2209 f j\"\n    proof (rule notI)\n      assume \"j \u2208 f j\"\n      with \u2039?S = f j\u203a have \"j \u2208 ?S\"\n        by (rule ssubst)\n      then have \"j \u2209 f j\"\n        by (rule CollectD)\n      then show False\n        using \u2039j \u2208 f j\u203a by (rule notE)\n    qed\n  qed\n  ultimately show False\n    by (rule notE)\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\ntheorem\n  fixes f :: \"'\u03b1 \u21d2 '\u03b1 set\"\n  shows \"\u00ac surj f\"\nproof\n  assume \"surj f\"\n  let ?S = \"{i. i \u2209 f i}\"\n  have \"\u2203 j. ?S = f j\" using \u2039surj f\u203a by (simp only: surjD)\n  then obtain j where \"?S = f j\" by (rule exE)\n  have \"j \u2209 ?S\"\n  proof\n    assume \"j \u2208 ?S\"\n    then have \"j \u2209 f j\" by simp\n    with \u2039?S = f j\u203a have \"j \u2209 ?S\" by simp\n    then show False using \u2039j \u2208 ?S\u203a by simp\n  qed\n  moreover\n  have \"j \u2208 ?S\"\n  proof\n    show \"j \u2209 f j\"\n    proof\n      assume \"j \u2208 f j\"\n      with \u2039?S = f j\u203a have \"j \u2208 ?S\" by simp\n      then have \"j \u2209 f j\" by simp\n      then show False using \u2039j \u2208 f j\u203a by simp\n    qed\n  qed\n  ultimately show False by simp\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\n\ntheorem\n  fixes f :: \"'\u03b1 \u21d2 '\u03b1 set\"\n  shows \"\u00ac surj f\"\nproof (rule notI)\n  assume \"surj f\"\n  let ?S = \"{i. i \u2209 f i}\"\n  have \"\u2203 j. ?S = f j\"\n    using \u2039surj f\u203a by (simp only: surjD)\n  then obtain j where \"?S = f j\"\n    by (rule exE)\n  have \"j \u2208 ?S = (j \u2209 f j)\"\n    by (rule mem_Collect_eq)\n  also have \"\u2026 = (j \u2209 ?S)\"\n    by (simp only: \u2039?S = f j\u203a)\n  finally show False\n    by (simp only: simp_thms(10))\nqed\n\n(* 5\u00aa demostraci\u00f3n *)\n\ntheorem\n  fixes f :: \"'\u03b1 \u21d2 '\u03b1 set\"\n  shows \"\u00ac surj f\"\nproof\n  assume \"surj f\"\n  let ?S = \"{i. i \u2209 f i}\"\n  have \"\u2203 j. ?S = f j\" using \u2039surj f\u203a by (simp only: surjD)\n  then obtain j where \"?S = f j\" by (rule exE)\n  have \"j \u2208 ?S = (j \u2209 f j)\" by simp\n  also have \"\u2026 = (j \u2209 ?S)\" using \u2039?S = f j\u203a by simp\n  finally show False by simp\nqed\n\n(* 6\u00aa demostraci\u00f3n *)\n\ntheorem\n  fixes f :: \"'\u03b1 \u21d2 '\u03b1 set\"\n  shows \"\u00ac surj f\"\n  unfolding surj_def\n  by best\n\nend\n<\/pre>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. En los monoides, los inversos a la izquierda y a la derecha son iguales<\/h3>\n<p>Un <a href=\"https:\/\/en.wikipedia.org\/wiki\/Monoid\">monoide<\/a> es un conjunto junto con una operaci\u00f3n binaria que es asociativa y tiene elemento neutro.<\/p>\n<p>En Lean4, est\u00e1 definida la clase de los monoides (como <code>Monoid<\/code>) y sus propiedades caracter\u00edsticas son<\/p>\n<pre lang=\"lean\">\n   mul_assoc : (a * b) * c = a * (b * c)\n   one_mul :   1 * a = a\n   mul_one :   a * 1 = a\n<\/pre>\n<p>Demostrar que si &#92;(M&#92;) es un monoide, &#92;(a \u2208 M&#92;), &#92;(b&#92;) es un inverso de &#92;(a&#92;) por la izquierda y &#92;(c&#92;) es un inverso de &#92;(a&#92;) por la derecha, entonces &#92;(b = c&#92;).<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Defs\n\nvariable {M : Type} [Monoid M]\nvariable {a b c : M}\n\nexample\n  (hba : b * a = 1)\n  (hac : a * c = 1)\n  : b = c :=\nby sorry\n<\/pre>\n<h4>5.1. Demostraci\u00f3n en lenguaje natural<\/h4>\n<p>Por la siguiente cadena de igualdades<br \/>\n&#92;begin{align}<br \/>\n   b &amp;= b * 1          &amp;&amp;&#92;text{[por mul_one]} &#92;&#92;<br \/>\n     &amp;= b * (a * c)    &amp;&amp;&#92;text{[por hip\u00f3tesis]} &#92;&#92;<br \/>\n     &amp;= (b * a) * c    &amp;&amp;&#92;text{[por mul_assoc]} &#92;&#92;<br \/>\n     &amp;= 1 * c          &amp;&amp;&#92;text{[por hip\u00f3tesis]} &#92;&#92;<br \/>\n     &amp;= c              &amp;&amp;&#92;text{[por one_mul]} &#92;&#92;<br \/>\n&#92;end{align}<\/p>\n<h4>5.2. Demostraciones con Lean4<\/h4>\n<pre lang=\"lean\">\nimport Mathlib.Algebra.Group.Defs\n\nvariable {M : Type} [Monoid M]\nvariable {a b c : M}\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hba : b * a = 1)\n  (hac : a * c = 1)\n  : b = c :=\ncalc b = b * 1       := (mul_one b).symm\n     _ = b * (a * c) := congrArg (b * .) hac.symm\n     _ = (b * a) * c := (mul_assoc b a c).symm\n     _ = 1 * c       := congrArg (. * c) hba\n     _ = c           := one_mul c\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hba : b * a = 1)\n  (hac : a * c = 1)\n  : b = c :=\ncalc b  = b * 1       := by aesop\n      _ = b * (a * c) := by aesop\n      _ = (b * a) * c := (mul_assoc b a c).symm\n      _ = 1 * c       := by aesop\n      _ = c           := by aesop\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hba : b * a = 1)\n  (hac : a * c = 1)\n  : b = c :=\nby\n  rw [\u2190one_mul c]\n  -- \u22a2 b = 1 * c\n  rw [\u2190hba]\n  -- \u22a2 b = (b * a) * c\n  rw [mul_assoc]\n  -- \u22a2 b = b * (a * c)\n  rw [hac]\n  -- \u22a2 b = b * 1\n  rw [mul_one b]\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hba : b * a = 1)\n  (hac : a * c = 1)\n  : b = c :=\nby rw [\u2190one_mul c, \u2190hba, mul_assoc, hac, mul_one b]\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample\n  (hba : b * a = 1)\n  (hac : a * c = 1)\n  : b = c :=\nleft_inv_eq_right_inv hba hac\n\n-- Lemas usados\n-- ============\n\n-- #check (left_inv_eq_right_inv : b * a = 1 \u2192 a * c = 1 \u2192 b = c)\n-- #check (mul_assoc a b c : (a * b) * c = a * (b * c))\n-- #check (mul_one a : a * 1 = a)\n-- #check (one_mul a : 1 * a = a)\n<\/pre>\n<p>Se puede interactuar con las demostraciones anteriores en <a href=\"https:\/\/live.lean-lang.org\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus2\/main\/src\/En_los_monoides_los_inversos_a_la_izquierda_y_a_la_derecha_son_iguales.lean\">Lean 4 Web<\/a>.<\/p>\n<h4>5.3. Demostraciones con Isabelle\/HOL<\/h4>\n<pre lang=\"isar\">\ntheory En_los_monoides_los_inversos_a_la_izquierda_y_a_la_derecha_son_iguales\nimports Main\nbegin\n\ncontext monoid\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"b * a = 1\"\n          \"a * c = 1\"\n  shows   \"b = c\"\nproof -\n  have      \"b  = b * 1\"      by (simp only: right_neutral)\n  also have \"\u2026 = b * (a * c)\" by (simp only: \u2039a * c = 1\u203a)\n  also have \"\u2026 = (b * a) * c\" by (simp only: assoc)\n  also have \"\u2026 = 1 * c\"       by (simp only: \u2039b * a = 1\u203a)\n  also have \"\u2026 = c\"           by (simp only: left_neutral)\n  finally show \"b = c\"        by this\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"b * a = 1\"\n          \"a * c = 1\"\n  shows   \"b = c\"\nproof -\n  have      \"b  = b * 1\"      by simp\n  also have \"\u2026 = b * (a * c)\" using \u2039a * c = 1\u203a by simp\n  also have \"\u2026 = (b * a) * c\" by (simp add: assoc)\n  also have \"\u2026 = 1 * c\"       using \u2039b * a = 1\u203a by simp\n  also have \"\u2026 = c\"           by simp\n  finally show \"b = c\"        by this\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\n\nlemma\n  assumes \"b * a = 1\"\n          \"a * c = 1\"\n  shows   \"b = c\"\n  using assms\n  by (metis assoc left_neutral right_neutral)\n\nend\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. Imagen de la interseccion general mediante aplicaciones inyectivas 2. Imagen inversa de la uni\u00f3n general 3. Imagen inversa de la intersecci\u00f3n general 4. Teorema de Cantor 5. En los monoides, los inversos a la izquierda y a la derecha son&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"default","_kad_post_title":"default","_kad_post_layout":"default","_kad_post_sidebar_id":"","_kad_post_content_style":"default","_kad_post_vertical_padding":"default","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[1],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8186"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=8186"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8186\/revisions"}],"predecessor-version":[{"id":8189,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/8186\/revisions\/8189"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=8186"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=8186"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=8186"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}