limsSup_bot

Mathlib.Order.LiminfLimsup

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

English

For a complete lattice, the limsSup of the bottom filter equals the bottom element.

Русский

Для полной решетки limsSup нижнего фильтра равен нижнему элементу.

LaTeX

$$$ \\operatorname{limsSup}(\\bot) = \\bot $$$

Lean4

@[simp]
theorem limsSup_bot : limsSup (⊥ : Filter α) = ⊥ :=
  bot_unique <| sInf_le <| by simp

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

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

Разделы

Аффилиация

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