Demostrar con Lean4 que
\n\[ s \u222a (s \u2229 t) = s \]<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Set.Basic\nopen Set\nvariable {\u03b1 : Type}\nvariable (s t : Set \u03b1)\n\nexample : s \u222a (s \u2229 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 \u222a (s \u2229 t) \u2194 x \u2208 s] \]
\ny lo haremos demostrando las dos implicaciones.<\/p>\n
(\u27f9) Sea \(x \u2208 s \u222a (s \u2229 t)\). Entonces, \(x \u2208 s\) \u00f3 \(x \u2208 s \u2229 t\). En ambos casos, \(x \u2208 s\).<\/p>\n
(\u27f8) Sea \(x \u2208 s\). Entonces, \(x \u2208 s \u2229 t\) y, por tanto, \(x \u2208 s \u222a (s \u2229 t)\).<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Basic\nopen Set\n\nvariable {\u03b1 : Type}\nvariable (s t : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a (s \u2229 t) = s :=\nby\n ext x\n -- x : \u03b1\n -- \u22a2 x \u2208 s \u222a (s \u2229 t) \u2194 x \u2208 s\n constructor\n . -- \u22a2 x \u2208 s \u222a (s \u2229 t) \u2192 x \u2208 s\n intro hx\n -- hx : x \u2208 s \u222a (s \u2229 t)\n -- \u22a2 x \u2208 s\n rcases hx with (xs | xst)\n . -- xs : x \u2208 s\n exact xs\n . -- xst : x \u2208 s \u2229 t\n exact xst.1\n . -- \u22a2 x \u2208 s \u2192 x \u2208 s \u222a (s \u2229 t)\n intro xs\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 s \u222a (s \u2229 t)\n left\n -- \u22a2 x \u2208 s\n exact xs\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a (s \u2229 t) = s :=\nby\n ext x\n -- x : \u03b1\n -- \u22a2 x \u2208 s \u222a s \u2229 t \u2194 x \u2208 s\n exact \u27e8fun hx \u21a6 Or.elim hx id And.left,\n fun xs \u21a6 Or.inl xs\u27e9\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a (s \u2229 t) = s :=\nby\n ext x\n -- x : \u03b1\n -- \u22a2 x \u2208 s \u222a (s \u2229 t) \u2194 x \u2208 s\n constructor\n . -- \u22a2 x \u2208 s \u222a (s \u2229 t) \u2192 x \u2208 s\n rintro (xs | \u27e8xs, -\u27e9) <;>\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 s\n exact xs\n . -- \u22a2 x \u2208 s \u2192 x \u2208 s \u222a (s \u2229 t)\n intro xs\n -- xs : x \u2208 s\n -- \u22a2 x \u2208 s \u222a s \u2229 t\n left\n -- \u22a2 x \u2208 s\n exact xs\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \u222a (s \u2229 t) = s :=\nsup_inf_self\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c : Prop)\n-- #check (And.left : a \u2227 b \u2192 a)\n-- #check (Or.elim : a \u2228 b \u2192 (a \u2192 c) \u2192 (b \u2192 c) \u2192 c)\n-- #check (sup_inf_self : s \u222a (s \u2229 t) = s)\n<\/pre>\n