English
Let p be a property on positive naturals. If for every k, assuming p holds for all m < k implies p(k), then p holds for all n ∈ ℕ⁺.
Русский
Пусть p — свойство на ℕ⁺. Если для каждого k верно: из того, что для всех m < k верно p(m), следует p(k), тогда p выполняется для всех n ∈ ℕ⁺.
LaTeX
$$$\\forall P:\\mathbb{N}^+ \\to \\mathrm{Prop},\\ (\\forall n:\\mathbb{N}^+,\\ (\\forall m:\\mathbb{N}^+, m < n \\rightarrow P m) \\rightarrow P n) \\rightarrow \\forall n:\\mathbb{N}^+, P n$$$
Lean4
/-- Strong induction on `ℕ+`. -/
def strongInductionOn {p : ℕ+ → Sort*} (n : ℕ+) : (∀ k, (∀ m, m < k → p m) → p k) → p n
| IH => IH _ fun a _ => strongInductionOn a IH
termination_by n.1
