induction_on — Mathlib

English

Applying ofAntisymmetrization and then toAntisymmetrization returns the original representative.

Русский

Применение ofAntisymmetrization затем toAntisymmetrization возвращает исходного представителя.

LaTeX

$$$\operatorname{toAntisymmetrization}(r)(\operatorname{ofAntisymmetrization}(r)\ a) = a$$$

Lean4

@[elab_as_elim]
protected theorem induction_on {p : Antisymmetrization α r → Prop} (a : Antisymmetrization α r)
    (h : ∀ a, p <| toAntisymmetrization r a) : p a :=
  Quotient.inductionOn' a h

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