{"id":1717,"date":"2023-10-20T06:00:12","date_gmt":"2023-10-20T04:00:12","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1717"},"modified":"2023-10-17T18:07:05","modified_gmt":"2023-10-17T16:07:05","slug":"20-oct-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/20-oct-23\/","title":{"rendered":"Si r \u2286 s y s \u2286 t, entonces r \u2286 t"},"content":{"rendered":"

Demostrar con Lean4 que si \(r \u2286 s\) y \(s \u2286 t\), entonces \(r \u2286 t\).<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 : Type _}\nvariable (r s t : Set \u03b1)\n\nexample\n  (rs : r \u2286 s)\n  (st : s \u2286 t)\n  : r \u2286 t :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n

\n1\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Tenemos que demostrar que
\n\[ (\u2200 x) [x \u2208 r \u2192 x \u2208 t] \]
\nSea \(x\) tal que
\n\[ x \u2208 r \]
\nPuesto que \(r \u2286 s\), se tiene que
\n\[ x \u2208 s \]
\ny, puesto que \(s \u2286 t), se tiene que
\n\[ x \u2208 t \]
\nque es lo que ten\u00edamos que demostrar.<\/p>\n
2\u00aa demostraci\u00f3n en LN<\/b><\/p>\n
Tenemos que demostrar que
\n\[ (\u2200 x) [x \u2208 r \u2192 x \u2208 t] \]
\nSea \(x\) tal que
\n\[ x \u2208 r \]
\nTenemos que demostrar que
\n\[ x \u2208 t \]
\nque, puesto que \(s \u2286 t\), se reduce a
\n\[ x \u2208 s \]
\nque, puesto que \(r \u2286 s\), se redece a
\n\[ x \u2208 r \]
\nque es lo que hemos supuesto.<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Tactic\n\nopen Set\n\nvariable {\u03b1 : Type _}\nvariable (r s t : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (rs : r \u2286 s)\n  (st : s \u2286 t)\n  : r \u2286 t :=\nby\n  intros x xr\n  -- xr : x \u2208 r\n  have xs : x \u2208 s := rs xr\n  show x \u2208 t\n  exact st xs\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (rs : r \u2286 s)\n  (st : s \u2286 t)\n  : r \u2286 t :=\nby\n  intros x xr\n  -- x : \u03b1\n  -- xr : x \u2208 r\n  apply st\n  -- \u22a2 x \u2208 s\n  apply rs\n  -- \u22a2 x \u2208 r\n  exact xr\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (rs : r \u2286 s)\n  (st : s \u2286 t)\n  : r \u2286 t :=\nfun _ xr \u21a6 st (rs xr)\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (rs : r \u2286 s)\n  (st : s \u2286 t)\n  : r \u2286 t :=\n-- by exact?\nSubset.trans rs st\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (rs : r \u2286 s)\n  (st : s \u2286 t)\n  : r \u2286 t :=\nby tauto\n\n-- Lemas usados\n-- ============\n\n-- #check (Subset.trans : r \u2286 s \u2192 s \u2286 t \u2192 r \u2286 t)\n<\/pre>\n
Demostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
Referencias<\/b><\/p>\n