cauchy_induction — Mathlib

English

Let P be a property on naturals. If P(n+1) implies P(n) and seed holds, then for any f: ℕ→ℕ with a suitable growth condition, P(n) holds for all n.

Русский

Пусть P — свойство над натуральными. Если P(n+1) ⇒ P(n) и база выполняется, то для любой f: ℕ→ℕ с условием роста P(n) выполняется для всех n.

LaTeX

$$$\\text{Cauchy induction: }(h),(seed),(hs),(f),(hf) \\Rightarrow \\forall n, P(n)$$$

Lean4

theorem cauchy_induction (h : ∀ n, P (n + 1) → P n) (seed : ℕ) (hs : P seed) (f : ℕ → ℕ)
    (hf : ∀ x, seed ≤ x → P x → x < f x ∧ P (f x)) (n : ℕ) : P n :=
  seed.cauchy_induction' h hs (fun x hl hx => ⟨f x, hf x hl hx⟩) n

Похожие утверждения