coe_eq_univ

Mathlib.Order.UpperLower.CompleteLattice

URI: https://scilib.ai/kg/mathlib#UpperSet.coe_eq_univ

English

A UpperSet equals the bottom if and only if its underlying set is the universe.

Русский

Верхнее множество равно нулю тогда, когда его носитель равен всем элементам.

LaTeX

$$(s : Set α) = \mathrm{univ} \\iff s = \bot$$

Lean4

@[simp, norm_cast]
theorem coe_eq_univ : (s : Set α) = univ ↔ s = ⊥ := by simp [SetLike.ext'_iff]

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

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

Разделы

Аффилиация

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