isCoboundedUnder_ge — Mathlib

English

If l is bounded under r, then l is coboundedUnder (flip r).

Русский

Если l ограничено по r, то l является coboundedUnder (flip r).

LaTeX

$$$\forall {α γ} {r : α \to α \to Prop} {u}, [IsTrans α r] [l.NeBot] (h : l.IsBoundedUnder r u) : l.IsCoboundedUnder (flip r) u.$$$

Lean4

theorem isCoboundedUnder_ge {u : γ → α} {l : Filter γ} [Preorder α] [NeBot l] (h : l.IsBoundedUnder (· ≤ ·) u) :
    l.IsCoboundedUnder (· ≥ ·) u :=
  h.isCoboundedUnder_flip

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