inductionOn — Mathlib

English

Induction on two quotient arguments: from mk x and mk y for all x,y to general q,q'.

Русский

Индукция по двум аргументам квазифракций: из mk x и mk y для всех x,y к общим q,q'.

LaTeX

$$$ \\forall q:\\, T2Quotient X,\\forall q': T2Quotient Y,\\ (\\forall x:\\, X)(\\forall y:\\, Y),\\ P( T2Quotient.mk x, T2Quotient.mk y) \\Rightarrow P(q,q')$$$

Lean4

@[elab_as_elim]
protected theorem inductionOn {motive : T2Quotient X → Prop} (q : T2Quotient X) (h : ∀ x, motive (T2Quotient.mk x)) :
    motive q :=
  Quotient.inductionOn q h

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