lean_workbook_plus_70613

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Note that, $f:N \rightarrow N$ and $f$ is a strictly increasing function. So, $f(1) \ge 1$ . Since, $f(1)<f(2)$ , so, $f(2)>1 \Rightarrow f(2)\ge 2$ . Assume that $f(m) \ge m$ for some natural $m \ge 1$ . So, $f(m+1) > f(m) \ge m \Rightarrow f(m+1)\ge (m+1)$ . Hence, by induction on $n \in \mathbb{N}$ , we have, $f(n) \ge n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_70613  (n : ℕ)
  (f : ℕ → ℕ)
  (h₀ : ∀ x y, x < y → f x < f y)
  (h₁ : f 1 ≥ 1) :
  f n ≥ n   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph