card_of_subsingleton — Mathlib

English

If α is a subsingleton, then Nat.card α = 1 (provided a chosen element is available).

Русский

Если α является подсубодиненным множеством, то Nat.card α = 1 (при наличии элемента).

LaTeX

$$$$ \text{Subsingleton}(\alpha) \Rightarrow |\alpha| = 1 $$$$

Lean4

theorem card_of_subsingleton (a : α) [Subsingleton α] : Nat.card α = 1 :=
  by
  letI := Fintype.ofSubsingleton a
  rw [card_eq_fintype_card, Fintype.card_ofSubsingleton a]

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