isBounded_ge_atTop

Mathlib.Order.Filter.IsBounded

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

English

In a nonempty preorder with a top element, the atTop filter is bounded below by ≥.

Русский

В непустом упорядоченном множестве с верхней гранью фильтр atTop ограничен снизу по ≥.

LaTeX

$$$(atTop : Filter \alpha).IsBounded(\ge)$$$

Lean4

theorem isBounded_ge_atTop : (atTop : Filter α).IsBounded (· ≥ ·) :=
  ‹Nonempty α›.elim fun a => ⟨a, eventually_ge_atTop _⟩

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

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

Разделы

Аффилиация

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