latticeClosure_subset_closure

Mathlib.Order.BooleanSubalgebra

URI: https://scilib.ai/kg/mathlib#BooleanSubalgebra.latticeClosure_subset_closure

English

The lattice closure of s is contained in the closure of s.

Русский

Латис Closure s ⊆ closure s.

LaTeX

$$$\\mathrm{latticeClosure}(s) \\subseteq \\mathrm{closure}(s)$$$

Lean4

theorem latticeClosure_subset_closure : latticeClosure s ⊆ closure s :=
  latticeClosure_min subset_closure (closure s).isSublattice

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

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

Разделы

Аффилиация

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