univ_unique — Mathlib

English

If α has a unique element, then the universal finite set in α is the singleton containing that unique element.

Русский

Если у α имеется единственный элемент, то Finset.univ α — единичное множество, содержащие этот элемент.

LaTeX

$$$(\mathrm{univ} : \mathrm{Finset} \alpha) = \{ \mathrm{default} \}$$$

Lean4

@[simp]
theorem univ_unique [Unique α] : (univ : Finset α) = { default } :=
  Finset.ext fun x => iff_of_true (mem_univ _) <| mem_singleton.2 <| Subsingleton.elim x default

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