isCobounded_ge_of_top

Mathlib.Order.Filter.IsBounded

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

English

In a structure with a top element, every filter is cobounded below with respect to ≥.

Русский

В структуре с верхней границей каждый фильтр кобондирован ниже относительно ≥.

LaTeX

$$$[LE \alpha] [OrderTop \alpha] \{f: Filter \alpha\} : f.IsCobounded(≥)$$$

Lean4

theorem isCobounded_ge_of_top [LE α] [OrderTop α] {f : Filter α} : f.IsCobounded (· ≥ ·) :=
  ⟨⊤, fun _ _ => le_top⟩

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

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

Разделы

Аффилиация

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