sSup_lowerBounds

Mathlib.Order.Filter.Defs

URI: https://scilib.ai/kg/mathlib#Filter.sSup_lowerBounds

English

The supremum of the lower bounds of a family s of filters equals the infimum of s.

Русский

Супремум нижних границ множества фильтров s равен инфимууму самого множества.

LaTeX

$$$\\operatorname{sSup}(\\operatorname{lowerBounds} s) = \\operatorname{sInf} s$$$

Lean4

protected theorem sSup_lowerBounds (s : Set (Filter α)) : sSup (lowerBounds s) = sInf s := by simp [sInf, Filter.sInf]

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

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

Разделы

Аффилиация

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