decreasing_induction_of_infinite — Mathlib

English

Let P: ℕ→Prop. If P(n+1) implies P(n) for all n, and the set {x | P x} is Infinite, then P(n) holds for all n.

Русский

Пусть P: ℕ→Prop. Если P(n+1) ⇒ P(n) для всех n и множество {x | P x} бесконечно, то P(n) верно для всех n.

LaTeX

$$$\\forall P\\ (\\forall n, P(n+1) \\Rightarrow P(n))\\;\\to\\; (\\{x \\mid P x\\}.Infinite) \\Rightarrow \\forall n, P(n)$$$

Lean4

theorem decreasing_induction_of_infinite (h : ∀ n, P (n + 1) → P n) (hP : {x | P x}.Infinite) (n : ℕ) : P n :=
  Nat.decreasing_induction_of_not_bddAbove h (mt BddAbove.finite hP) n

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