isCoboundedUnder_le_of_le — Mathlib

English

If l is a filter on ι with NeBot and for all i, x ≤ f i, then IsCoboundedUnder (≤) l f.

Русский

Если для всех i верно x ≤ f(i), то IsCoboundedUnder ≤ l f.

LaTeX

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

Lean4

theorem isCoboundedUnder_le_of_le [Preorder α] (l : Filter ι) [NeBot l] {f : ι → α} {x : α} (hf : ∀ i, x ≤ f i) :
    IsCoboundedUnder (· ≤ ·) l f :=
  isCoboundedUnder_le_of_eventually_le l (Eventually.of_forall hf)

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