isBoundedUnder_le_comp — Mathlib

English

If v is antitone and l is bounded below by u with respect to ≥, then l is bounded above by v ∘ u with respect to ≤.

Русский

Если v антитонна и l ограничен снизу по ≥ через u, то l ограничен сверху по ≤ через v∘u.

LaTeX

$$[Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β} (hv : Antitone v) (hl : l.IsBoundedUnder (\ge) u) : l.IsBoundedUnder (\le) (v ∘ u)$$

Lean4

theorem _root_.Antitone.isBoundedUnder_le_comp [Preorder α] [Preorder β] {l : Filter γ} {u : γ → α} {v : α → β}
    (hv : Antitone v) (hl : l.IsBoundedUnder (· ≥ ·) u) : l.IsBoundedUnder (· ≤ ·) (v ∘ u) :=
  hl.comp (swap hv)

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