latticeClosure_univ

Mathlib.Order.SupClosed

URI: https://scilib.ai/kg/mathlib#latticeClosure_univ

English

latticeClosure of the universal set is universal.

Русский

Замыкание по решётке универсального множества совпадает с ним самим.

LaTeX

$$$\mathrm{latticeClosure}(\mathrm{Set.univ}) = \mathrm{Set.univ}$$$

Lean4

@[simp]
theorem latticeClosure_univ : latticeClosure (Set.univ : Set α) = Set.univ := by simp

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

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

Разделы

Аффилиация

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