isBoundedUnder_le_comp_iff — Mathlib

English

If g is monotone and Tendsto g atBot atBot, then IsBoundedUnder (≥) l (g ∘ f) is equivalent to IsBoundedUnder (≥) l f.

Русский

Если g монотонна и Tendsto g atBot atBot, то ограниченность IsBoundedUnder (≥) g∘f эквивалентна ограниченности IsBoundedUnder (≥) f.

LaTeX

$$$\operatorname{IsBoundedUnder}(\ge, l)(g\circ f) \iff \operatorname{IsBoundedUnder}(\ge, l)f$$$

Lean4

theorem isBoundedUnder_le_comp_iff [Nonempty β] [LinearOrder β] [Preorder γ] [NoMaxOrder γ] {g : β → γ} {f : α → β}
    {l : Filter α} (hg : Antitone g) (hg' : Tendsto g atBot atTop) :
    IsBoundedUnder (· ≤ ·) l (g ∘ f) ↔ IsBoundedUnder (· ≥ ·) l f :=
  hg.dual_right.isBoundedUnder_ge_comp_iff hg'

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