card_ofSubsingleton — Mathlib

English

If α is a Subsingleton, then its card is 1.

Русский

Если α однозначен, то его кардинал равен 1.

LaTeX

$$$ \\operatorname{card}(\\alpha) = 1. $$$

Lean4

/-- Note: this lemma is specifically about `Fintype.ofSubsingleton`. For a statement about
arbitrary `Fintype` instances, use either `Fintype.card_le_one_iff_subsingleton` or
`Fintype.card_unique`. -/
theorem card_ofSubsingleton (a : α) [Subsingleton α] : @Fintype.card _ (ofSubsingleton a) = 1 :=
  rfl

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