Demostrar con Lean4 que
\n\[ s \\setminus (t \u222a u) \u2286 (s \\setminus t) \\setminus 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 \u222a u) \u2286 (s \\ t) \\ u :=\nby sorry\n<\/pre>\n<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(x \u2208 s \\setminus (t \u222a u)\). Entonces,
\n\begin{align}
\n &x \u2208 s \tag{1} \\
\n &x \u2209 t \u222a u \tag{2} \\
\n\end{align}
\nTenemos que demostrar que \(x \u2208 (s \\setminus t) \\setminus u\); es decir, que se verifican las relaciones
\n\begin{align}
\n &x \u2208 s \\setminus t \tag{3} \\
\n &x \u2209 u \tag{4}
\n\end{align}
\nPara demostrar (3) tenemos que demostrar las relaciones
\n\begin{align}
\n &x \u2208 s \tag{5} \\
\n &x \u2209 t \tag{6}
\n\end{align}
\nLa (5) se tiene por la (1). Para demostrar la (6), supongamos que \(x \u2208 t\); entonces, \(x \u2208 t \u222a u\), en contracci\u00f3n con (2). Para demostrar la (4), supongamos que \(x \u2208 u\); entonces, \(x \u2208 t \u222a u\), en contracci\u00f3n con (2).<\/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 \u222a u) \u2286 (s \\ t) \\ u :=\nby\n intros x hx\n -- x : \u03b1\n -- hx : x \u2208 s \\ (t \u222a u)\n -- \u22a2 x \u2208 (s \\ t) \\ u\n constructor\n . -- \u22a2 x \u2208 s \\ t\n constructor\n . -- \u22a2 x \u2208 s\n exact hx.1\n . -- \u22a2 \u00acx \u2208 t\n intro xt\n -- xt : x \u2208 t\n -- \u22a2 False\n apply hx.2\n -- \u22a2 x \u2208 t \u222a u\n left\n -- \u22a2 x \u2208 t\n exact xt\n . -- \u22a2 \u00acx \u2208 u\n intro xu\n -- xu : x \u2208 u\n -- \u22a2 False\n apply hx.2\n -- \u22a2 x \u2208 t \u222a u\n right\n -- \u22a2 x \u2208 u\n exact xu\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \\ (t \u222a u) \u2286 (s \\ t) \\ u :=\nby\n rintro x \u27e8xs, xntu\u27e9\n -- x : \u03b1\n -- xs : x \u2208 s\n -- xntu : \u00acx \u2208 t \u222a u\n -- \u22a2 x \u2208 (s \\ t) \\ u\n constructor\n . -- \u22a2 x \u2208 s \\ t\n constructor\n . -- \u22a2 x \u2208 s\n exact xs\n . -- \u00acx \u2208 t\n intro xt\n -- xt : x \u2208 t\n -- \u22a2 False\n exact xntu (Or.inl xt)\n . -- \u22a2 \u00acx \u2208 u\n intro xu\n -- xu : x \u2208 u\n -- \u22a2 False\n exact xntu (Or.inr xu)\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \\ (t \u222a u) \u2286 (s \\ t) \\ u :=\n fun _ \u27e8xs, xntu\u27e9 \u21a6 \u27e8\u27e8xs, fun xt \u21a6 xntu (Or.inl xt)\u27e9,\n fun xu \u21a6 xntu (Or.inr xu)\u27e9\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \\ (t \u222a u) \u2286 (s \\ t) \\ u :=\nby\n rintro x \u27e8xs, xntu\u27e9\n -- x : \u03b1\n -- xs : x \u2208 s\n -- xntu : \u00acx \u2208 t \u222a u\n -- \u22a2 x \u2208 (s \\ t) \\ u\n aesop\n\n-- 5\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \\ (t \u222a u) \u2286 (s \\ t) \\ u :=\nby intro ; aesop\n\n-- 6\u00aa demostraci\u00f3n\n-- ===============\n\nexample : s \\ (t \u222a u) \u2286 (s \\ t) \\ 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