isBoundedUnder_le_comp — Mathlib

English

If v is monotone, and l is bounded under ≤ by u, then l is bounded under ≤ by v ∘ u.

Русский

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

LaTeX

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

Lean4

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

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