Si (∀ε > 0)[x ≤ ε], entonces x ≤ 0
Demostrar con Lean4 que si \((∀ε > 0)[x ≤ ε]\), entonces \(x ≤ 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable (x : ℝ) example (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by sorry |
Demostración en lenguaje natural
Basta demostrar que \(x ≯ 0\). Para ello, supongamos que \(x > 0\) y vamos a demostrar que
\[ ¬(∀ε)[ε > 0 → x ≤ ε] \tag{1} \]
que es una contradicción con la hipótesis. Interiorizando la negación, (1) es equivalente a
\[ (∃ε)[ε > 0 ∧ ε < x] \tag{2} \]
Para demostrar (2), elegimos \(ε = \dfrac{x}{2}\) ya que, como \(x > 0\), se tiene
\[ 0 < \dfrac{x}{2} < x\]
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 |
import Mathlib.Data.Real.Basic variable (x : ℝ) -- 1ª demostración -- =============== example (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by apply le_of_not_gt -- ⊢ ¬x > 0 intro hx0 -- hx0 : x > 0 -- ⊢ False apply absurd h -- ⊢ ¬∀ (ε : ℝ), ε > 0 → x ≤ ε push_neg -- ⊢ ∃ ε, ε > 0 ∧ ε < x use x /2 -- ⊢ x / 2 > 0 ∧ x / 2 < x constructor { show x / 2 > 0 exact half_pos hx0 } { show x / 2 < x exact half_lt_self hx0 } -- 2ª demostración -- =============== example (x : ℝ) (h : ∀ ε > 0, x ≤ ε) : x ≤ 0 := by contrapose! h -- ⊢ ∃ ε, ε > 0 ∧ ε < x use x / 2 -- ⊢ x / 2 > 0 ∧ x / 2 < x constructor { show x / 2 > 0 exact half_pos h } { show x / 2 < x exact half_lt_self h } -- Lemas usados -- ============ -- variable (a b : ℝ) -- variable (p q : Prop) -- #check (le_of_not_gt : ¬a > b → a ≤ b) -- #check (half_lt_self : 0 < a → a / 2 < a) -- #check (half_pos : 0 < a → 0 < a / 2) -- #check (absurd : p → ¬p → q) |
Demostraciones interactivas
Se puede interactuar con las demostraciones anteriores en Lean 4 Web.
Referencias
- J. Avigad y P. Massot. Mathematics in Lean, p. 32.
