inductionOn₂ — Mathlib

English

Same as inductionOn₂; used for two-argument induction on quotients.

Русский

То же самое, что и inductionOn₂; используется для двуматричной индукции по квазифракциям.

LaTeX

$$$ \\forall {X} {Y} [TopologicalSpace X] [TopologicalSpace Y]\\, {motive: T2Quotient X \\to T2Quotient Y \\to Prop}, (q: T2Quotient X) (q': T2Quotient Y),\\ (\\forall x y, motive (T2Quotient.mk x)(T2Quotient.mk y)) \\Rightarrow motive q q'$$

Lean4

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

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