Demostrar con Lean4 que
\n\[ s \u2229 (s \u222a t) = s \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\nopen Set\nvariable {\u03b1 : Type}\nvariable (s t : Set \u03b1)\n\nexample : s \u2229 (s \u222a t) = s :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Tenemos que demostrar que
\n\[ (\u2200 x)[x \u2208 s \u2229 (s \u222a t) \u2194 x \u2208 s] \]
\ny lo haremos demostrando las dos implicaciones.<\/p>\n
(\u27f9) Sea \(x \u2208 s \u2229 (s \u222a t)\). Entonces, \(x \u2208 s\).<\/p>\n
(\u27f8) Sea \(x \u2208 s\). Entonces, \(x \u2208 s \u222a t\) y, por tanto, \(x \u2208 s \u2229 (s \u222a t)\).<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\nopen Set\n\nvariable {\u03b1 : Type}\nvariable (s t : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2229 (s \u222a t) = s :=\nby\n ext x\n -- x : \u03b1\n -- \u22a2 x \u2208 s \u2229 (s \u222a t) \u2194 x \u2208 s\n constructor\n . -- \u22a2 x \u2208 s \u2229 (s \u222a t) \u2192 x \u2208 s\n intros h\n -- h : x \u2208 s \u2229 (s \u222a t)\n -- \u22a2 x \u2208 s\n exact h.1\n . -- \u22a2 x \u2208 s \u2192 x \u2208 s \u2229 (s \u222a t)\n intro xs\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 s \u2229 (s \u222a t)\n constructor\n . -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 x \u2208 s \u222a t\n left\n -- \u22a2 x \u2208 s\n exact xs\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2229 (s \u222a t) = s :=\nby\n ext x\n -- x : \u03b1\n -- \u22a2 x \u2208 s \u2229 (s \u222a t) \u2194 x \u2208 s\n constructor\n . -- \u22a2 x \u2208 s \u2229 (s \u222a t) \u2192 x \u2208 s\n intro h\n -- h : x \u2208 s \u2229 (s \u222a t)\n -- \u22a2 x \u2208 s\n exact h.1\n . -- \u22a2 x \u2208 s \u2192 x \u2208 s \u2229 (s \u222a t)\n intro xs\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 s \u2229 (s \u222a t)\n constructor\n . -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 x \u2208 s \u222a t\n exact (Or.inl xs)\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2229 (s \u222a t) = s :=\nby\n ext\n -- x : \u03b1\n -- \u22a2 x \u2208 s \u2229 (s \u222a t) \u2194 x \u2208 s\n exact \u27e8fun h \u21a6 h.1,\n fun xs \u21a6 \u27e8xs, Or.inl xs\u27e9\u27e9\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2229 (s \u222a t) = s :=\nby\n ext\n -- x : \u03b1\n -- \u22a2 x \u2208 s \u2229 (s \u222a t) \u2194 x \u2208 s\n exact \u27e8And.left,\n fun xs \u21a6 \u27e8xs, Or.inl xs\u27e9\u27e9\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2229 (s \u222a t) = s :=\nby\n ext x\n -- x : \u03b1\n -- \u22a2 x \u2208 s \u2229 (s \u222a t) \u2194 x \u2208 s\n constructor\n . -- \u22a2 x \u2208 s \u2229 (s \u222a t) \u2192 x \u2208 s\n rintro \u27e8xs, -\u27e9\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 x \u2208 s \u2192 x \u2208 s \u2229 (s \u222a t)\n intro xs\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 s \u2229 (s \u222a t)\n use xs\n -- \u22a2 x \u2208 s \u222a t\n left\n -- \u22a2 x \u2208 s\n exact xs\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2229 (s \u222a t) = s :=\nby\n apply subset_antisymm\n . -- \u22a2 s \u2229 (s \u222a t) \u2286 s\n rintro x \u27e8hxs, -\u27e9\n -- x : \u03b1\n -- hxs : x \u2208 s\n -- \u22a2 x \u2208 s\n exact hxs\n . -- \u22a2 s \u2286 s \u2229 (s \u222a t)\n intros x hxs\n -- x : \u03b1\n -- hxs : x \u2208 s\n -- \u22a2 x \u2208 s \u2229 (s \u222a t)\n exact \u27e8hxs, Or.inl hxs\u27e9\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2229 (s \u222a t) = s :=\ninf_sup_self\n\n-- 8\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u2229 (s \u222a t) = s :=\nby aesop\n\n-- Lemas usados\n-- ============\n\n-- variable (a b : Prop)\n-- #check (And.left : a \u2227 b \u2192 a)\n-- #check (Or.inl : a \u2192 a \u2228 b)\n-- #check (inf_sup_self : s \u2229 (s \u222a t) = s)\n-- #check (subset_antisymm : s \u2286 t \u2192 t \u2286 s \u2192 s = t)\n<\/pre>\n