isBoundedUnder_ge_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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