{"id":1865,"date":"2023-12-15T06:00:14","date_gmt":"2023-12-15T04:00:14","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=1865"},"modified":"2023-12-08T14:41:36","modified_gmt":"2023-12-08T12:41:36","slug":"15-dic-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/15-dic-23\/","title":{"rendered":"Si (\u2203z \u2208 \u211d)[x < z < y], entonces x < y"},"content":{"rendered":"\n

Demostrar con Lean4 que si \((\u2203z \u2208 \u211d)[x < z < y]\), entonces \(x < y\).<\/p>\n

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

\nimport Mathlib.Data.Real.Basic\nvariable (x y : \u211d)\n\nexample : (\u2203 z : \u211d, x < z \u2227 z < y) \u2192 x < y :=\nby sorry\n<\/pre>\n
<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
Sea \(z\) tal que verifica las siguientes relaciones:
\n\begin{align}
\n   x < z \tag{1} \\
\n   z < y \tag{2}
\n\end{align}
\nAplicando la propiedad transitiva a (1) y (2) se tiene que
\n\[ x < y \]<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n
\nimport Mathlib.Data.Real.Basic\nvariable (x y : \u211d)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (\u2203 z : \u211d, x < z \u2227 z < y) \u2192 x < y :=\nby\n  rintro \u27e8z, h1 : x < z, h2 : z < y\u27e9\n  show x < y\n  exact lt_trans h1 h2\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (\u2203 z : \u211d, x < z \u2227 z < y) \u2192 x < y :=\nby\n  rintro \u27e8z, h1, h2\u27e9\n  exact lt_trans h1 h2\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (\u2203 z : \u211d, x < z \u2227 z < y) \u2192 x < y :=\nfun \u27e8_, h1, h2\u27e9 \u21a6 lt_trans h1 h2\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c : \u211d)\n-- #check (lt_trans : a < b \u2192 b < c \u2192 a < c)\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