Strictly_Increasing_Sequence_of_Natural_Numbers
Provedproofwikisequences
Let be the set of natural numbers without zero Let be strictly increasing sequence in . Then
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Strictly_Increasing_Sequence_of_Natural_Numbers (f : ℕ → ℕ) (hf : StrictMono f) : ∀ n, n ≤ f n := by sorry
Source