range_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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