Propiedad arquimediana de los números reales
Demostrar la propiedad arquimediana de los números reales; es decir, que para cualquier \(ε ∈ ℝ\) con \(0 < ε\), existe \(N ∈ ℕ\) tal que \(1/ε < N\).
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {ε : ℝ} variable (h : 0 < ε) example : ∃ (N : ℕ), 1 / ε < N := by sorry
1. Demostración en lenguaje natural
Sea \(N = ⌈1/ε⌉ + 1\). Entonces, \begin{align} 1/ε &≤ ⌈1/ε⌉ \newline &< ⌈1/ε⌉ + 1 \newline &= N \newline \end{align} Por lo tanto, \(1/ε < N\).
2. Demostraciones con Lean4
import Mathlib.Data.Real.Basic import Mathlib.Tactic variable {ε : ℝ} variable (h : 0 < ε) -- 1ª demostración -- =============== example : ∃ (N : ℕ), 1 / ε < N := by -- ⊢ ∃ N, 1 / ε < ↑N use ⌈1 / ε⌉₊ + 1 -- ⊢ 1 / ε < ↑(⌈1 / ε⌉₊ + 1) have fact : 1 / ε ≤ ⌈1 / ε⌉₊ := by bound -- fact : 1 / ε ≤ ↑⌈1 / ε⌉₊ push_cast -- ⊢ 1 / ε < ↑⌈1 / ε⌉₊ + 1 bound -- 2ª demostración -- =============== example : ∃ (N : ℕ), 1 / ε < N := by -- ⊢ ∃ N, 1 / ε < ↑N use ⌈1 / ε⌉₊ + 1 -- ⊢ 1 / ε < ↑(⌈1 / ε⌉₊ + 1) have fact : 1 / ε ≤ ⌈1 / ε⌉₊ := Nat.le_ceil (1 / ε) -- fact : 1 / ε ≤ ↑⌈1 / ε⌉₊ push_cast -- ⊢ 1 / ε < ↑⌈1 / ε⌉₊ + 1 apply lt_of_le_of_lt fact -- ⊢ ↑⌈1 / ε⌉₊ < ↑⌈1 / ε⌉₊ + 1 exact lt_add_one _ -- 3ª demostración -- =============== example : ∃ (N : ℕ), 1 / ε < N := by -- ⊢ ∃ N, 1 / ε < ↑N use ⌈1 / ε⌉₊ + 1 -- ⊢ 1 / ε < ↑(⌈1 / ε⌉₊ + 1) push_cast -- ⊢ 1 / ε < ↑⌈1 / ε⌉₊ + 1 calc 1 / ε ≤ ↑⌈1 / ε⌉₊ := Nat.le_ceil (1 / ε) _ < ↑⌈1 / ε⌉₊ + 1 := lt_add_one _ -- 4ª demostración -- =============== example : ∃ (N : ℕ), 1 / ε < N := by -- ⊢ ∃ N, 1 / ε < ↑N use ⌈1 / ε⌉₊ + 1 -- ⊢ 1 / ε < ↑(⌈1 / ε⌉₊ + 1) push_cast -- ⊢ 1 / ε < ↑⌈1 / ε⌉₊ + 1 exact lt_of_le_of_lt (Nat.le_ceil (1 / ε)) (lt_add_one _) -- 5ª demostración -- =============== example : ∃ (N : ℕ), 1 / ε < N := exists_nat_gt (1 / ε) -- 6ª demostración -- =============== example : ∃ (N : ℕ), 1 / ε < N := by -- ⊢ ∃ N, 1 / ε < ↑N use ⌈1 / ε⌉₊ + 1 -- ⊢ 1 / ε < ↑(⌈1 / ε⌉₊ + 1) calc 1 / ε ≤ (⌈1 / ε⌉₊ : ℝ) := Nat.le_ceil (1 / ε) _ < (⌈1 / ε⌉₊ : ℝ) + 1 := lt_add_one _ _ = ↑(⌈1 / ε⌉₊ + 1) := by norm_num -- Lemas usados -- ============ variable (a b c : ℝ) #check (Nat.le_ceil a : a ≤ ↑⌈a⌉₊) #check (exists_nat_gt (1 / ε) : ∃ n : ℕ, 1 / ε < ↑n) #check (lt_add_one a : a < a + 1) #check (lt_of_le_of_lt : a ≤ b → b < c → a < c)