English
There is an induction principle for Antisymmetrization: to prove a property for every element of Antisymmetrization α r it suffices to prove it for all representatives via toAntisymmetrization r.
Русский
Для Antisymmetrization α r существует принцип индукции: чтобы доказать свойство для каждого элемента Antisymmetrization, достаточно доказать его на представителях через toAntisymmetrization r.
LaTeX
$$$\forall p:\mathrm{Antisymmetrization}(\alpha, r) \to \text{Prop}, \big(\forall a:\alpha, p\big|\!\operatorname{toAntisymmetrization}(r,a)\big) \Rightarrow p(q) \,\text{for all } q$$$
Lean4
@[elab_as_elim]
protected theorem ind {p : Antisymmetrization α r → Prop} : (∀ a, p <| toAntisymmetrization r a) → ∀ q, p q :=
Quot.ind
