inductionOn₃ — Mathlib

English

For any predicate p on three cardinals, if p holds for all triples ( #α, #β, #γ ), then p holds for ( c1, c2, c3 ).

Русский

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

LaTeX

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

Lean4

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

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