subset_supClosure

Mathlib.Order.SupClosed

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

English

For every set s in a join-semilattice, s is contained in its supremum-closure, i.e. s ⊆ supClosure(s).

Русский

Для любого множества s в полугруппе с операцией взятия верхнего объединения (join) выполняется s ⊆ supClosure(s).

LaTeX

$$$s \\subseteq \\operatorname{supClosure}(s)$$$

Lean4

@[simp]
theorem subset_supClosure {s : Set α} : s ⊆ supClosure s :=
  supClosure.le_closure _

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

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

Разделы

Аффилиация

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