inductionOn — Mathlib

English

For any property p on cardinals, if p holds for all cardinals of the form #α, then p holds for every cardinal c.

Русский

Для любого свойства p, определённого на кардиналах, если p верно для всех кардиналов вида #α, то p верно и для любого кардинала c.

LaTeX

$$$\forall p:\mathrm{Cardinal} \to \mathrm{Prop},\ \forall c,\ (\forall \alpha,\ p(\#\alpha)) \to p(c)$$$

Lean4

@[elab_as_elim]
theorem inductionOn {p : Cardinal → Prop} (c : Cardinal) (h : ∀ α, p #α) : p c :=
  Quotient.inductionOn c h

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