isCoboundedUnder_le — Mathlib

English

If l is bounded below by ≥ with respect to u, then l is coboundedUnder ≤ with respect to u.

Русский

Если лямбда-перавода ограничена снизу по ≥ относительно u, то она coboundedUnder ≤ относительно u.

LaTeX

$$$\forall {u} {l} [Preorder α] [NeBot l] (h : l.IsBoundedUnder (≥) u) : l.IsCoboundedUnder (≤) u.$$$

Lean4

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

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