univ_unique

Mathlib.Data.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.univ_unique

English

If α has a unique element, then univ is the singleton {default}.

Русский

Если у α есть одиночный элемент, то универсуум равен множеству {default}.

LaTeX

$$$[\text{Unique } \alpha] : \mathrm{univ} = \{ \mathrm{default} \}$$$

Lean4

theorem univ_unique [Unique α] : @Set.univ α = { default } :=
  Set.ext fun x => iff_of_true trivial <| Subsingleton.elim x default

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru