instSubsingleton — Mathlib

English

If a type α is subsingleton (has at most one element), then its opposite type αᵒᵖ also has at most one element.

Русский

Если тип α имеет не более одного элемента, то его противоположный тип αᵒᵖ также имеет не более одного элемента.

LaTeX

$$$$ \forall \alpha, \operatorname{Subsingleton}(\alpha) \Rightarrow \operatorname{Subsingleton}(\alpha^{op}) $$$$

Lean4

instance [Subsingleton α] : Subsingleton αᵒᵖ :=
  unop_injective.subsingleton

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