instSubsingletonAntisymmetrization

English

If the base type α is a subsingleton, then the antisymmetrization Antisymmetrization α r is also a subsingleton.

Русский

Если базовый тип α является подселектной (пододиночным), то Antisymmetrization α r также подселектен.

LaTeX

$$$\text{Subsingleton}(\alpha) \Rightarrow \text{Subsingleton}(\operatorname{Antisymmetrization}(\alpha, r))$$$

Lean4

instance [Subsingleton α] : Subsingleton (Antisymmetrization α r) := by unfold Antisymmetrization; infer_instance

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