Si a es una cota superior de f y c ≥ 0, entonces ca es una cota superior de cf
Demostrar con Lean4 que si \(a\) es una cota superior de \(f\) y \(c ≥ 0\), entonces \(ca\) es una cota superior de \(cf\).
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 -- (CotaSuperior f a) se verifica si a es una cota superior de f. def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a variable {f : ℝ → ℝ} variable {c : ℝ} example (hfa : CotaSuperior f a) (h : c ≥ 0) : CotaSuperior (fun x ↦ c * f x) (c * a) := by sorry |
Demostración en lenguaje natural
Se usará el lema
\[ \{b ≤ c, 0 ≤ a\} ⊢ ab ≤ ac \tag{L1} \]
Tenemos que demostrar que
\[ (∀ y ∈ ℝ) cf(y) ≤ ca \]
Sea \(y ∈ R\). Puesto que \(a\) es una cota de \(f\), se tiene que
\[ f(y) ≤ a \]
que, junto con \(c ≥ 0\), por el lema L1 nos da
\[ cf(y) ≤ ca \]
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 |
import Mathlib.Data.Real.Basic -- (CotaSuperior f a) se verifica si a es una cota superior de f. def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a variable {f : ℝ → ℝ} variable {c : ℝ} -- 1ª demostración example (hfa : CotaSuperior f a) (h : c ≥ 0) : CotaSuperior (fun x ↦ c * f x) (c * a) := by intro y -- y : ℝ -- ⊢ (fun x => c * f x) y ≤ c * a have ha : f y ≤ a := hfa y calc (fun x => c * f x) y = c * f y := by rfl _ ≤ c * a := mul_le_mul_of_nonneg_left ha h -- 2ª demostración example (hfa : CotaSuperior f a) (h : c ≥ 0) : CotaSuperior (fun x ↦ c * f x) (c * a) := by intro y calc (fun x => c * f x) y = c * f y := by rfl _ ≤ c * a := mul_le_mul_of_nonneg_left (hfa y) h -- 3ª demostración example (hfa : CotaSuperior f a) (h : c ≥ 0) : CotaSuperior (fun x ↦ c * f x) (c * a) := by intro y show (fun x => c * f x) y ≤ c * a exact mul_le_mul_of_nonneg_left (hfa y) h -- 4ª demostración lemma CotaSuperior_mul (hfa : CotaSuperior f a) (h : c ≥ 0) : CotaSuperior (fun x ↦ c * f x) (c * a) := fun y ↦ mul_le_mul_of_nonneg_left (hfa y) h -- Lemas usados -- ============ -- variable (c : ℝ) -- #check (mul_le_mul_of_nonneg_left : b ≤ c → 0 ≤ a → a * b ≤ a * c) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 29.
