isCobounded_le

Mathlib.Order.Filter.IsBounded

URI: https://scilib.ai/kg/mathlib#Filter.IsBounded.isCobounded_le

English

If a filter f is bounded below by ≥, then it is cobounded above by ≤.

Русский

Если фильтр f ограничен снизу по ≥, то он cobounded снизу по ≤.

LaTeX

$$$\forall f\, [\text{NeBot } f],\ (f.IsBounded (\ge)) \Rightarrow (f.IsCobounded (\le)).$$$

Lean4

theorem isCobounded_le [Preorder α] [NeBot f] (h : f.IsBounded (· ≥ ·)) : f.IsCobounded (· ≤ ·) :=
  h.isCobounded_flip

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

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

Разделы

Аффилиация

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