isBoundedUnder_ge_comp_iff — Mathlib

English

For an antitone map g with Tendsto to bottom, there is an equivalence between IsBoundedUnder (≤) for g ∘ f and IsBoundedUnder (≥) for f.

Русский

Для антитонной g и Tendsto к нижней границе существует эквивалентность: IsBoundedUnder (≤) g∘f ↔ IsBoundedUnder (≥) f.

LaTeX

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

Lean4

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

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