closure_mono

Mathlib.Order.BooleanSubalgebra

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

English

If s ⊆ t then closure(s) ≤ closure(t).

Русский

Если s ⊆ t, то closure(s) ≤ closure(t).

LaTeX

$$$s \\subseteq t \\Rightarrow \\mathrm{closure}(s) \\le \\mathrm{closure}(t)$$$

Lean4

theorem closure_mono (hst : s ⊆ t) : closure s ≤ closure t :=
  sInf_le_sInf fun _L ↦ hst.trans

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

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

Разделы

Аффилиация

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