isCobounded_ge

Mathlib.Order.Filter.IsBounded

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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