La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g
Demostrar con Lean4 que si \(f\) y \(g\) son funciones de \(ℝ\) en \(ℝ\), entonces la suma de una cota inferior de \(f\) y una cota inferior de \(g\) es una cota inferior de \(f+g\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import Mathlib.Data.Real.Basic -- (CotaInferior f a) expresa que a es una cota inferior de f. def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variable (f g : ℝ → ℝ) variable (a b : ℝ) example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := by sorry |
Demostración en lenguaje natural
Se usará el siguiente lema
\[ a ≤ b → c ≤ d → a + c ≤ b + d \tag{L1} \]
Por la definición de cota inferior, hay que demostrar que
\[ (∀ x ∈ ℝ) [a + b ≤ f(x) + g(x)] \tag{1} \]
Para ello, sea \(x ∈ R\). Puesto que es \(a\) es una cota inferior de \(f\), se tiene que
\[ a ≤ f(x) \tag{2} \]
y, puesto que \(b\) es una cota inferior de \(g\), se tiene que
\[ b ≤ g(x) \tag{3} \]
De (2) y (3), por L1, se tiene que
\[ a + b ≤ f(x) + g(x) \]
que es lo que había que demostrar.
Demostraciones con Lean4
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 |
import Mathlib.Data.Real.Basic -- (CotaInferior f a) expresa que a es una cota inferior de f. def CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x variable (f g : ℝ → ℝ) variable (a b : ℝ) -- 1ª demostración example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := by have h1 : ∀ x, a + b ≤ f x + g x { intro x have h1a : a ≤ f x := hfa x have h1b : b ≤ g x := hgb x show a + b ≤ f x + g x exact add_le_add h1a h1b } show CotaInferior (f + g) (a + b) exact h1 -- 2ª demostración example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := by have h1 : ∀ x, a + b ≤ f x + g x { intro x show a + b ≤ f x + g x exact add_le_add (hfa x) (hgb x) } show CotaInferior (f + g) (a + b) exact h1 -- 3ª demostración example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := by intro x dsimp apply add_le_add . apply hfa . apply hgb -- 4ª demostración example (hfa : CotaInferior f a) (hgb : CotaInferior g b) : CotaInferior (f + g) (a + b) := λ x ↦ add_le_add (hfa x) (hgb x) -- Lemas usados -- ============ -- variable (c d : ℝ) -- #check (add_le_add : a ≤ b → c ≤ d → a + c ≤ b + d) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 25.
