isBoundedUnder_ge_comp_iff — Mathlib

English

For an antitone map g with Tendsto to the bottom, boundedness of g ∘ f under ≥ is equivalent to boundedness of f under ≥ after dualization.

Русский

Для антитонической отображения g с тенденцией к нижней границе, ограниченность g∘f при ≥ эквивалентна ограниченности f после двойственной перестановки порядка.

LaTeX

$$$IsBoundedUnder(\ge)(l)(g\circ f) \iff IsBoundedUnder(\le)(l)f$$$

Lean4

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

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