univ_eq_singleton_of_card_one — Mathlib

English

If α is finite and its cardinality is 1, then the universe is a singleton: univ = {x} for the unique x ∈ α.

Русский

Если α конечен и |α| = 1, то множество универа равняется одному элементу: univ = {x}.

LaTeX

$$$|\alpha| = 1 \Rightarrow (\mathrm{univ} : \mathrm{Finset}\,\alpha) = \{ x \}$$$

Lean4

theorem univ_eq_singleton_of_card_one {α} [Fintype α] (x : α) (h : Fintype.card α = 1) : (univ : Finset α) = { x } :=
  by
  symm
  apply eq_of_subset_of_card_le (subset_univ { x })
  apply le_of_eq
  simp [h, Finset.card_univ]

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