decreasing_induction_of_not_bddAbove

English

If for all n, P(n+1) implies P(n) and the set {x | P(x)} is not bounded above, then P(n) holds for every n.

Русский

Если для всех n выполняется P(n+1) ⇒ P(n) и множество {x | P(x)} не ограничено сверху, то P(n) верно для всех n.

LaTeX

$$$\\forall n\\, P(n+1) \\Rightarrow P(n) \\quad\\text{and}\\quad \\neg\\mathrm{BddAbove}\\{x \\mid P(x)\\} \\Rightarrow \\forall n, P(n)$$$

Lean4

theorem decreasing_induction_of_not_bddAbove (h : ∀ n, P (n + 1) → P n) (hP : ¬BddAbove {x | P x}) (n : ℕ) : P n :=
  let ⟨_, hm, hl⟩ := not_bddAbove_iff.1 hP n
  decreasingInduction (fun _ _ => h _) hm hl.le

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