induction — Mathlib

English

If a property P holds for an ordinal i whenever it holds for all smaller ordinals, then P holds for every ordinal i.

Русский

Если свойство P верно для ординала i при условии верности P для всех меньших ординалов, то P верно для каждого ординала i.

LaTeX

$$$\\text{If } P: \\mathrm{Ordinal} \\to \\mathrm{Prop} \\text{ satisfies } (\\forall j, (\\forall k

Lean4

/-- Reformulation of well-founded induction on ordinals as a lemma that works with the
`induction` tactic, as in `induction i using Ordinal.induction with | h i IH => ?_`. -/
theorem induction {p : Ordinal.{u} → Prop} (i : Ordinal.{u}) (h : ∀ j, (∀ k, k < j → p k) → p j) : p i :=
  lt_wf.induction i h

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