Si para cada a existe un x tal que f(x) < a, entonces f no tiene cota inferior
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 inferior.
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 CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x def acotadaInf (f : ℝ → ℝ) : Prop := ∃ a, CotaInferior f a variable (f : ℝ → ℝ) example (h : ∀ a, ∃ x, f x < a) : ¬ acotadaInf f := by sorry |
Demostración en lenguaje natural
Supongamos que \(f\) tiene cota inferior. Sea \(b\) una de dichas cotas inferiores. Por la hipótesis, existe un \(x\) tal que \(f(x) < b\). Además, como \(b\) es una cota inferior de \(f\), \(b ≤ f(x)\) 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 CotaInferior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, a ≤ f x def acotadaInf (f : ℝ → ℝ) : Prop := ∃ a, CotaInferior f a variable (f : ℝ → ℝ) -- 1ª demostración example (h : ∀ a, ∃ x, f x < a) : ¬ acotadaInf f := by intros hf -- hf : acotadaInf f -- ⊢ False cases' hf with b hb -- b : ℝ -- hb : CotaInferior f b cases' h b with x hx -- x : ℝ -- hx : f x < b have : b ≤ f x := hb x linarith -- 2ª demostración example (h : ∀ a, ∃ x, f x < a) : ¬ acotadaInf f := by intros hf -- hf : acotadaInf f -- ⊢ False rcases hf with ⟨b, hb : CotaInferior f b⟩ rcases h b with ⟨x, hx : f x < b⟩ have : b ≤ f x := 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.
