range_comp — Mathlib

English

If range f is bounded above and g is monotone, then range (g ∘ f) is bounded above.

Русский

Если диапазон f ограничен сверху и g монотонна, то диапазон g∘f ограничен сверху.

LaTeX

$$$ \\operatorname{BddAbove}(\\mathrm{range} f) \\rightarrow \\operatorname{Monotone} g \\rightarrow \\operatorname{BddAbove}(\\mathrm{range}(g \\circ f)) $$$

Lean4

theorem range_comp {γ : Type*} [Preorder β] [Preorder γ] {f : α → β} {g : β → γ} (hf : BddAbove (range f))
    (hg : Monotone g) : BddAbove (range (fun x => g (f x))) :=
  by
  change BddAbove (range (g ∘ f))
  simpa only [Set.range_comp] using hg.map_bddAbove hf

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