Demostrar con Lean4 que si \(a\) es una cota superior de \(s\) y \(a \u2264 b\), entonces \(b\) es una cota superior de \(s\).<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Tactic\n\nvariable {\u03b1 : Type _} [PartialOrder \u03b1]\nvariable (s : Set \u03b1)\nvariable (a b : \u03b1)\n\n-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.\ndef CotaSupConj (s : Set \u03b1) (a : \u03b1) :=\n \u2200 {x}, x \u2208 s \u2192 x \u2264 a\n\nexample\n (h1 : CotaSupConj s a)\n (h2 : a \u2264 b)\n : CotaSupConj s b :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nTenemos que demostrar que
\n\[ (\u2200 x) [x \u2208 s \u2192 x \u2264 b] \]
\nSea \(x\) tal que \(x \u2208 s\). Entonces,
\n\begin{align}
\n x &\u2264 a &&\text{[porque \(a\) es una cota superior de \(s\)]} \\
\n &\u2264 b
\n\end{align}
\nPor tanto, \(x \u2264 b\).<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Tactic\n\nvariable {\u03b1 : Type _} [PartialOrder \u03b1]\nvariable (s : Set \u03b1)\nvariable (a b : \u03b1)\n\n-- (CotaSupConj s a) afirma que a es una cota superior del conjunto s.\ndef CotaSupConj (s : Set \u03b1) (a : \u03b1) :=\n \u2200 {x}, x \u2208 s \u2192 x \u2264 a\n\n-- 1\u00aa demostraci\u00f3n\nexample\n (h1 : CotaSupConj s a)\n (h2 : a \u2264 b)\n : CotaSupConj s b :=\nby\n intro x (xs : x \u2208 s)\n have h3 : x \u2264 a := h1 xs\n show x \u2264 b\n exact le_trans h3 h2\n\n-- 2\u00aa demostraci\u00f3n\nexample\n (h1 : CotaSupConj s a)\n (h2 : a \u2264 b)\n : CotaSupConj s b :=\nby\n intro x (xs : x \u2208 s)\n calc x \u2264 a := h1 xs\n _ \u2264 b := h2\n-\n-- Lemas usados\n-- ============\n\n-- variable (c : \u03b1)\n-- #check (le_trans : a \u2264 b \u2192 b \u2264 c \u2192 a \u2264 c)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n