inductionOn₂ — Mathlib

English

For any predicate p on two cardinals, if p holds for all pairs ( #α, #β ), then p holds for ( c1, c2 ).

Русский

Для любого предиката p на двух кардиналах, если p верно для всех пар (#α, #β), то верно и для (c1, c2).

LaTeX

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

Lean4

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

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