Demostrar con Lean4 que
\n\[ (s \\setminus t) \\setminus u \u2286 s \\setminus (t \u222a u) \]<\/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 u : Set \u03b1)\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(x \u2208 (s \\setminus t) \\setminus u\). Entonces, se tiene que
\n\begin{align}
\n &x \u2208 s \tag{1} \\
\n &x \u2209 t \tag{2} \\
\n &x \u2209 u \tag{3}
\n\end{align}
\nTenemos que demostrar que
\n\[ x \u2208 s \\setminus (t \u222a u) \]
\npero, por (1), se reduce a
\n\[ x \u2209 t \u222a u \]
\nque se verifica por (2) y (3).<\/p>\n
2. Demostraciones con Lean4<\/h2>\n\nimport Mathlib.Data.Set.Basic\nopen Set\n\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 (s \\ t) \\ u\n -- \u22a2 x \u2208 s \\ (t \u222a u)\n rcases hx with \u27e8hxst, hxnu\u27e9\n -- hxst : x \u2208 s \\ t\n -- hxnu : \u00acx \u2208 u\n rcases hxst with \u27e8hxs, hxnt\u27e9\n -- hxs : x \u2208 s\n -- hxnt : \u00acx \u2208 t\n constructor\n . -- \u22a2 x \u2208 s\n exact hxs\n . -- \u22a2 \u00acx \u2208 t \u222a u\n by_contra hxtu\n -- hxtu : x \u2208 t \u222a u\n -- \u22a2 False\n rcases hxtu with (hxt | hxu)\n . -- hxt : x \u2208 t\n apply hxnt\n -- \u22a2 x \u2208 t\n exact hxt\n . -- hxu : x \u2208 u\n apply hxnu\n -- \u22a2 x \u2208 u\n exact hxu\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n rintro x \u27e8\u27e8hxs, hxnt\u27e9, hxnu\u27e9\n -- x : \u03b1\n -- hxnu : \u00acx \u2208 u\n -- hxs : x \u2208 s\n -- hxnt : \u00acx \u2208 t\n -- \u22a2 x \u2208 s \\ (t \u222a u)\n constructor\n . -- \u22a2 x \u2208 s\n exact hxs\n . -- \u22a2 \u00acx \u2208 t \u222a u\n by_contra hxtu\n -- hxtu : x \u2208 t \u222a u\n -- \u22a2 False\n rcases hxtu with (hxt | hxu)\n . -- hxt : x \u2208 t\n exact hxnt hxt\n . -- hxu : x \u2208 u\n exact hxnu hxu\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n rintro x \u27e8\u27e8xs, xnt\u27e9, xnu\u27e9\n -- x : \u03b1\n -- xnu : \u00acx \u2208 u\n -- xs : x \u2208 s\n -- xnt : \u00acx \u2208 t\n -- \u22a2 x \u2208 s \\ (t \u222a u)\n use xs\n -- \u22a2 \u00acx \u2208 t \u222a u\n rintro (xt | xu)\n . -- xt : x \u2208 t\n -- \u22a2 False\n contradiction\n . -- xu : x \u2208 u\n -- \u22a2 False\n contradiction\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n rintro x \u27e8\u27e8xs, xnt\u27e9, xnu\u27e9\n -- x : \u03b1\n -- xnu : \u00acx \u2208 u\n -- xs : x \u2208 s\n -- xnt : \u00acx \u2208 t\n -- \u22a2 x \u2208 s \\ (t \u222a u)\n use xs\n -- \u22a2 \u00acx \u2208 t \u222a u\n rintro (xt | xu) <;> contradiction\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n intro x xstu\n -- x : \u03b1\n -- xstu : x \u2208 (s \\ t) \\ u\n -- \u22a2 x \u2208 s \\ (t \u222a u)\n simp at *\n -- \u22a2 x \u2208 s \u2227 \u00ac(x \u2208 t \u2228 x \u2208 u)\n aesop\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby\n intro x xstu\n -- x : \u03b1\n -- xstu : x \u2208 (s \\ t) \\ u\n -- \u22a2 x \u2208 s \\ (t \u222a u)\n aesop\n\n-- 7\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \\ t) \\ u \u2286 s \\ (t \u222a u) :=\nby rw [diff_diff]\n\n-- Lema usado\n-- ==========\n\n-- #check (diff_diff : (s \\ t) \\ u = s \\ (t \u222a u))\n<\/pre>\n