Demostrar con Lean4 que la suma de dos funciones mon\u00f3tonas es mon\u00f3tona.<\/p>\n
Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n
\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\nexample\n (mf : Monotone f)\n (mg : Monotone g)\n : Monotone (f + g) :=\nby sorry\n<\/pre>\n<\/p>\n
Demostraci\u00f3n en lenguaje natural<\/b><\/p>\n
\nSe usar\u00e1 el siguiente lema:
\n\[ \{a \u2264 b, c \u2264 d\} \u22a2 a + c \u2264 b + d \tag{L1} \]<\/p>\n
Supongamos que \(f\) y \(g\) son mon\u00f3tonas y teneno que demostrar que \(f+g\) tambi\u00e9n lo es; que
\n\[ (\u2200 a,\ b \in \u211d) [a \u2264 b \u2192 (f + g)(a) \u2264 (f + g)(b)] \]
\nSean \(a, b \u2208 \u211d\) tales que
\n\[ a \u2264 b \tag{1} \]
\nEntonces, por ser \(f\) y \(g\) mon\u00f3tonas se tiene
\n\begin{align}
\n f(a) &\u2264 f(b) \tag{2} \\
\n g(a) &\u2264 g(b) \tag{3}
\n\end{align}
\nEntonces,
\n\begin{align}
\n (f + g)(a) &= f(a) + g(a) \\
\n &\u2264 f(b) + g(b) &&\text{[por L1, (2) y (3)]} \\
\n &= (f + g)(b)
\n\end{align}<\/p>\n
Demostraciones con Lean4<\/b><\/p>\n\nimport Mathlib.Data.Real.Basic\n\nvariable (f g : \u211d \u2192 \u211d)\n\n-- 1\u00aa demostraci\u00f3n\nexample\n (mf : Monotone f)\n (mg : Monotone g)\n : Monotone (f + g) :=\nby\n have h1 : \u2200 a b, a \u2264 b \u2192 (f + g) a \u2264 (f + g) b\n { intros a b hab\n have h2 : f a \u2264 f b := mf hab\n have h3 : g a \u2264 g b := mg hab\n calc (f + g) a\n = f a + g a := rfl\n _ \u2264 f b + g b := add_le_add h2 h3\n _ = (f + g) b := rfl }\n show Monotone (f + g)\n exact h1\n\n-- 2\u00aa demostraci\u00f3n\nexample\n (mf : Monotone f)\n (mg : Monotone g)\n : Monotone (f + g) :=\nby\n have h1 : \u2200 a b, a \u2264 b \u2192 (f + g) a \u2264 (f + g) b\n { intros a b hab\n calc (f + g) a\n = f a + g a := rfl\n _ \u2264 f b + g b := add_le_add (mf hab) (mg hab)\n _ = (f + g) b := rfl }\n show Monotone (f + g)\n exact h1\n\n-- 3\u00aa demostraci\u00f3n\nexample\n (mf : Monotone f)\n (mg : Monotone g)\n : Monotone (f + g) :=\nby\n have h1 : \u2200 a b, a \u2264 b \u2192 (f + g) a \u2264 (f + g) b\n { intros a b hab\n show (f + g) a \u2264 (f + g) b\n exact add_le_add (mf hab) (mg hab) }\n show Monotone (f + g)\n exact h1\n\n-- 4\u00aa demostraci\u00f3n\nexample\n (mf : Monotone f)\n (mg : Monotone g)\n : Monotone (f + g) :=\nby\n -- a b : \u211d\n -- hab : a \u2264 b\n intros a b hab\n apply add_le_add\n . -- f a \u2264 f b\n apply mf hab\n . -- g a \u2264 g b\n apply mg hab\n\n-- 5\u00aa demostraci\u00f3n\nexample\n (mf : Monotone f)\n (mg : Monotone g)\n : Monotone (f + g) :=\n\u03bb _ _ hab \u21a6 add_le_add (mf hab) (mg hab)\n\n-- Lemas usados\n-- ============\n\n-- variable (a b c d : \u211d)\n-- #check (add_le_add : a \u2264 b \u2192 c \u2264 d \u2192 a + c \u2264 b + d)\n<\/pre>\nDemostraciones interactivas<\/b><\/p>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\nReferencias<\/b><\/p>\n