isCoboundedUnder_ge_of_eventually_le

English

In a preorder, if l is a filter on ι with NeBot and f: ι → α satisfies eventually f i ≤ x, then IsCoboundedUnder (≥) l f.

Русский

В предпорядке, если l — фильтр на ι с NeBot и есть свойство, что f(i) ≤ x для большинства i, то IsCoboundedUnder ≥ l f.

LaTeX

$$$[Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α} (hf : ∀^ᶠ i in l, f i \le x) : IsCoboundedUnder (≥) l f.$$$

Lean4

theorem isCoboundedUnder_ge_of_eventually_le [Preorder α] (l : Filter ι) [NeBot l] {f : ι → α} {x : α}
    (hf : ∀ᶠ i in l, f i ≤ x) : IsCoboundedUnder (· ≥ ·) l f :=
  IsBoundedUnder.isCoboundedUnder_ge ⟨x, hf⟩

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