Demostrar con Lean4 que \(s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u)\).<\/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 u : Set \u03b1)\n\nexample :\n s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(x \u2208 s \u2229 (t \u222a u)\). Entonces se tiene que
\n\begin{align}
\n &x \u2208 s \tag{1} \\
\n &x \u2208 t \u222a u \tag{2}
\n\end{align}
\nLa relaci\u00f3n (2) da lugar a dos casos.<\/p>\n
Caso 1: Supongamos que \(x \u2208 t\). Entonces, por (1), \(x \u2208 s \u2229 t\) y, por tanto, \(x \u2208 (s \u2229 t) \u222a (s \u2229 u)\).<\/p>\n
Caso 2: Supongamos que \(x \u2208 u\). Entonces, por (1), \(x \u2208 s \u2229 u\) y, por tanto, \(x \u2208 (s \u2229 t) \u222a (s \u2229 u)\).<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Basic\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 s \u2229 (t \u222a u)\n -- \u22a2 x \u2208 s \u2229 t \u222a s \u2229 u\n rcases hx with \u27e8hxs, hxtu\u27e9\n -- hxs : x \u2208 s\n -- hxtu : x \u2208 t \u222a u\n rcases hxtu with (hxt | hxu)\n . -- hxt : x \u2208 t\n left\n -- \u22a2 x \u2208 s \u2229 t\n constructor\n . -- \u22a2 x \u2208 s\n exact hxs\n . -- hxt : x \u2208 t\n exact hxt\n . -- hxu : x \u2208 u\n right\n -- \u22a2 x \u2208 s \u2229 u\n constructor\n . -- \u22a2 x \u2208 s\n exact hxs\n . -- \u22a2 x \u2208 u\n exact hxu\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby\n rintro x \u27e8hxs, hxt | hxu\u27e9\n -- x : \u03b1\n -- hxs : x \u2208 s\n -- \u22a2 x \u2208 s \u2229 t \u222a s \u2229 u\n . -- hxt : x \u2208 t\n left\n -- \u22a2 x \u2208 s \u2229 t\n exact \u27e8hxs, hxt\u27e9\n . -- hxu : x \u2208 u\n right\n -- \u22a2 x \u2208 s \u2229 u\n exact \u27e8hxs, hxu\u27e9\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby\n rintro x \u27e8hxs, hxt | hxu\u27e9\n -- x : \u03b1\n -- hxs : x \u2208 s\n -- \u22a2 x \u2208 s \u2229 t \u222a s \u2229 u\n . -- hxt : x \u2208 t\n exact Or.inl \u27e8hxs, hxt\u27e9\n . -- hxu : x \u2208 u\n exact Or.inr \u27e8hxs, hxu\u27e9\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby\n intro x hx\n -- x : \u03b1\n -- hx : x \u2208 s \u2229 (t \u222a u)\n -- \u22a2 x \u2208 s \u2229 t \u222a s \u2229 u\n aesop\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample :\n s \u2229 (t \u222a u) \u2286 (s \u2229 t) \u222a (s \u2229 u) :=\nby rw [inter_union_distrib_left]\n<\/pre>\n