isCoboundedUnder_le_of_eventually_le

English

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

Русский

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

LaTeX

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

Lean4

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

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