Si para cada a existe un x tal que f(x) > a, entonces f no tiene cota superior
Demostrar con Lean4 que si \(f\) es una función de \(ℝ\) en \(ℝ\) tal que para cada \(a\) existe un \(x\) tal que \(f(x) > a\), entonces \(f\) no tiene cota superior.
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 def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) : Prop := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) example (h : ∀ a, ∃ x, f x > a) : ¬ acotadaSup f := by sorry |
Demostración en lenguaje natural
Supongamos que \(f\) tiene cota superior. Sea \(b\) una de dichas cotas superiores. Por la hipótesis, existe un \(x\) tal que \(f(x) > b\). Además, como \(b\) es una cota superior de \(f\), \(f(x) ≤ b\) que contradice la desigualdad anterior.
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 |
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) : Prop := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) -- 1ª demostración example (h : ∀ a, ∃ x, f x > a) : ¬ acotadaSup f := by intros hf -- hf : acotadaSup f -- ⊢ False cases' hf with b hb -- b : ℝ -- hb : CotaSuperior f b cases' h b with x hx -- x : ℝ -- hx : f x > b have : f x ≤ b := hb x linarith -- 2ª demostración theorem sinCotaSup (h : ∀ a, ∃ x, f x > a) : ¬ acotadaSup f := by intros hf -- hf : acotadaSup f -- ⊢ False rcases hf with ⟨b, hb : CotaSuperior f b⟩ rcases h b with ⟨x, hx : f x > b⟩ have : f x ≤ b := hb x linarith |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.
