Demostrar con Lean4 que para cualquier conjunto \(s\), \(s \u2286 s\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Tactic\n\nvariable {\u03b1 : Type _}\nvariable (s : Set \u03b1)\n\nexample : s \u2286 s :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nTenemos que demostrar que
\n\[ (\u2200 x) [x \u2208 s \u2192 \u00d7 \u2208 s] \]
\nSea \(x\) tal que
\n\[ x \u2208 s \tag{1} \]
\nEntonces, por (1), se tiene que
\n\[ x \u2208 s \]
\nque es lo que ten\u00edamos que demostrar.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Tactic\n\nvariable {\u03b1 : Type _}\nvariable (s : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\nexample : s \u2286 s :=\nby\n intro x xs\n exact xs\n\n-- 2\u00aa demostraci\u00f3n\nexample : s \u2286 s :=\n fun (x : \u03b1) (xs : x \u2208 s) \u21a6 xs\n\n-- 3\u00aa demostraci\u00f3n\nexample : s \u2286 s :=\n fun _ xs \u21a6 xs\n\n-- 4\u00aa demostraci\u00f3n\nexample : s \u2286 s :=\n -- by exact?\n rfl.subset\n\n-- 5\u00aa demostraci\u00f3n\nexample : s \u2286 s :=\nby rfl\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n