sInf_union

Mathlib.Order.CompleteLattice.Basic

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

English

The infimum of the union equals the meet of the infima: sInf(s ∪ t) = sInf(s) ⊓ sInf(t).

Русский

Infimum объединения равен произведению минимальных: sInf(s ∪ t) = sInf(s) ⊓ sInf(t).

LaTeX

$$$$ \operatorname{sInf}(s \cup t) = \operatorname{sInf}(s) \sqcap \operatorname{sInf}(t) $$$$

Lean4

theorem sInf_union {s t : Set α} : sInf (s ∪ t) = sInf s ⊓ sInf t :=
  ((isGLB_sInf s).union (isGLB_sInf t)).sInf_eq

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

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

Разделы

Аффилиация

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