lean_workbook_plus_49637
ProvedBecause f is strictly increasing, then
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_49637 (f : ℕ → ℕ) (hf: StrictMono f) : ∀ n, f n ≥ n := by sorry
Source
Because f is strictly increasing, then
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_49637 (f : ℕ → ℕ) (hf: StrictMono f) : ∀ n, f n ≥ n := by sorry