Si ¬(∀a)(∃x)[f(x) > a], entonces f está acotada superiormente
Demostrar con Lean4 que si \(¬(∀a)(∃x)[f(x) > a]\), entonces \(f\) está acotada superiormente.
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 : ℝ → ℝ) := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) example (h : ¬∀ a, ∃ x, f x > a) : acotadaSup f := by sorry |
Demostración en lenguaje natural
Tenemos que demostrar que \(f\) es acotada superiormente; es decir, que
\[ (∃a)(∀x)[f(x) ≤ a] \]
que es exactamente la fórmula obtenida interiorizando la negación en la hipótesis.
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 |
import Mathlib.Data.Real.Basic def CotaSuperior (f : ℝ → ℝ) (a : ℝ) : Prop := ∀ x, f x ≤ a def acotadaSup (f : ℝ → ℝ) := ∃ a, CotaSuperior f a variable (f : ℝ → ℝ) -- 1ª demostración -- =============== example (h : ¬∀ a, ∃ x, f x > a) : acotadaSup f := by unfold acotadaSup -- ⊢ ∃ a, CotaSuperior f a unfold CotaSuperior -- ⊢ ∃ a, ∀ (x : ℝ), f x ≤ a push_neg at h -- h : ∃ a, ∀ (x : ℝ), f x ≤ a exact h -- 2ª demostración -- =============== example (h : ¬∀ a, ∃ x, f x > a) : acotadaSup f := by unfold acotadaSup CotaSuperior -- ⊢ ∃ a, ∀ (x : ℝ), f x ≤ a push_neg at h -- h : ∃ a, ∀ (x : ℝ), f x ≤ a exact h -- 3ª demostración -- =============== example (h : ¬∀ a, ∃ x, f x > a) : acotadaSup f := by push_neg at h -- h : ∃ a, ∀ (x : ℝ), f x ≤ a exact h |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 34.
