ind_on — Mathlib

English

For any property C on ManyOneDegree, if C holds for allOf(p) for every p, then C holds for every d.

Русский

Для любого свойства C над ManyOneDegree, если C выполняется для всех p через конструктор of, то C выполняется для любого d.

LaTeX

$$$ \\forall C:\\\\ManyOneDegree\\to Prop, \\forall d:\\ManyOneDegree, (\\\\forall p:\\\\Set\\\\Nat, C(\\\\ManyOneDegree.of p)) \\\\Rightarrow C d $$$

Lean4

@[elab_as_elim]
protected theorem ind_on {C : ManyOneDegree → Prop} (d : ManyOneDegree) (h : ∀ p : Set ℕ, C (of p)) : C d :=
  Quotient.inductionOn' d h

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