isBounded_ge_of_bot — Mathlib

English

If α has an order with a bottom element, then any filter is cobounded below with respect to ≤.

Русский

Если у упорядоченного множества есть нулевой элемент, любой фильтр кобундирован снизу относительно ≤.

LaTeX

$$$[LE \alpha] [OrderBot \alpha] {f : Filter \alpha} : f.IsCobounded(≤)$$$

Lean4

theorem isBounded_ge_of_bot [LE α] [OrderBot α] {f : Filter α} : f.IsBounded (· ≥ ·) :=
  ⟨⊥, Eventually.of_forall fun _ => bot_le⟩

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