card_eq_one — Mathlib

English

If α has a unique inhabitant, then card α = 1.

Русский

Если у α есть единственный элемент, то card α = 1.

LaTeX

$$$ \\forall α\\ [FinEnum α] [Unique α],\\ \\operatorname{card}(α) = 1. $$$

Lean4

/-- Any enumeration of a type with unique inhabitant has length 1. -/
theorem card_eq_one (α : Type u) [FinEnum α] [Unique α] : card α = 1 :=
  card_eq_fintypeCard.trans <| Fintype.card_eq_one_iff_nonempty_unique.mpr ⟨‹_›⟩

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