lean_workbook_plus_71419
ProvedIf for all n ∈ N, then a ≤ b.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71419 (n : ℕ) (a b : ℝ) (hb : ∃ n, b < n) (hab : ∀ n, a ≤ b + 1/n) : a ≤ b := by sorry
Source
If for all n ∈ N, then a ≤ b.
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_71419 (n : ℕ) (a b : ℝ) (hb : ∃ n, b < n) (hab : ∀ n, a ≤ b + 1/n) : a ≤ b := by sorry