English
Let seed be a natural number and suppose we can always extend from x to a larger y with P(y) and still maintain a step relation. Then P holds at every n starting from seed.
Русский
Пусть есть базовый элемент и можно переходить к большему y, удовлетворяющему P(y), сохраняя шаг. Тогда P выполняется для всех n, начиная с seed.
LaTeX
$$$\\text{Cauchy induction'}(\\text{seed}, h, hs, hi, n)$$$
Lean4
theorem cauchy_induction' (seed : ℕ) (h : ∀ n, P (n + 1) → P n) (hs : P seed)
(hi : ∀ x, seed ≤ x → P x → ∃ y, x < y ∧ P y) (n : ℕ) : P n :=
by
apply Nat.decreasing_induction_of_infinite h fun hf => _
intro hf
obtain ⟨m, hP, hm⟩ := hf.exists_maximal ⟨seed, hs⟩
obtain ⟨y, hl, hy⟩ := hi m (le_of_not_gt <| not_lt_iff_le_imp_ge.2 <| hm hs) hP
exact hl.not_ge (hm hy hl.le)
