La función identidad no está acotada superiormente
Demostrar con Lean4 que la función identidad no está acotada superiormente.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 |
import src.Funcion_no_acotada_superiormente example : ¬ acotadaSup (fun x ↦ x) := by sorry |
Demostración en lenguaje natural
Usando el lema de ejercicio anterior (que afirma que si para cada \(a\), existe un \(x\) tal que \(f(x) > a\), entonces \(f\) no tiene cota superior) basta demostrar que
\[ (∀a ∈ ℝ)(∃x ∈ ℝ) [x > a] \]
Sea \(a ∈ ℝ\). Entonces \(a + 1 > a\) y, por tanto, \((∃x ∈ ℝ) [x > a]\).
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 |
import src.Funcion_no_acotada_superiormente -- 1ª demostración example : ¬ acotadaSup (fun x ↦ x) := by apply sinCotaSup -- ⊢ ∀ (a : ℝ), ∃ x, x > a intro a -- a : ℝ -- ⊢ ∃ x, x > a use a + 1 -- ⊢ a + 1 > a linarith -- 2ª demostración example : ¬ acotadaSup (fun x ↦ x) := by apply sinCotaSup -- ⊢ ∀ (a : ℝ), ∃ x, x > a intro a -- a : ℝ -- ⊢ ∃ x, x > a exact ⟨a + 1, by linarith⟩ -- 3ª demostración example : ¬ acotadaSup (fun x ↦ x) := by apply sinCotaSup -- ⊢ ∀ (a : ℝ), ∃ x, x > a exact fun a ↦ ⟨a + 1, by 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.
