latticeClosure_mono

Mathlib.Order.SupClosed

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

English

latticeClosure is monotone: if s ⊆ t then latticeClosure(s) ⊆ latticeClosure(t).

Русский

latticeClosure является монотонным: если s ⊆ t, то latticeClosure(s) ⊆ latticeClosure(t).

LaTeX

$$$s \subseteq t \to \mathrm{latticeClosure}(s) \subseteq \mathrm{latticeClosure}(t)$$$

Lean4

theorem latticeClosure_mono : Monotone (latticeClosure : Set α → Set α) :=
  latticeClosure.monotone

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

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

Разделы

Аффилиация

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