isCoboundedUnder_ge_of_le — Mathlib

English

In a preorder, if for all i, f i ≤ x, then IsCoboundedUnder (≥) l f.

Русский

В предпорядке, если для всех i выполняется f(i) ≤ x, то IsCoboundedUnder ≥ l f.

LaTeX

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

Lean4

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

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