induction — Mathlib

English

Let P be a predicate on Nimbers. If for every i, whenever P holds for all smaller Nimbers j < i, then P(i) holds, then P holds for all Nimbers.

Русский

Пусть P — предикат на Nimbers. Если для каждого i выполнение P(i) следует из того, что P(j) верно для всех j < i, тогда P выполняется для всех Nimbers.

LaTeX

$$$\forall P:\Nimber\to \mathrm{Prop},\ (\forall i:\Nimber,\ (\forall j

Lean4

/-- `Ordinal.induction` but for `Nimber`. -/
theorem induction {p : Nimber → Prop} : ∀ (i) (_ : ∀ j, (∀ k, k < j → p k) → p j), p i :=
  Ordinal.induction

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