English
If f maps into a β with a lower bound 0 and g is monotone on {x≥0}, then range(g∘f) is bounded above when range(f) is bounded above.
Русский
Если f лежит в β с нижней границей 0 и g монотона на {x≥0}, тогда диапазон g∘f ограничен сверху, если диапазон f ограничен сверху.
LaTeX
$$$\text{BddAbove}(\mathrm{range}\,f) \to (0 \le f) \to (\mathrm{MonotoneOn}\,g\,\{x \mid 0 \le x\}) \\to \mathrm{BddAbove}(\mathrm{range}\,(\lambda x. g(f(x))))$$$
Lean4
/-- A variant of `BddAbove.range_comp` that assumes that `f` is nonnegative and `g` is monotone on
nonnegative values. -/
theorem range_comp_of_nonneg {α β γ : Type*} [Nonempty α] [Preorder β] [Zero β] [Preorder γ] {f : α → β} {g : β → γ}
(hf : BddAbove (range f)) (hf0 : 0 ≤ f) (hg : MonotoneOn g {x : β | 0 ≤ x}) : BddAbove (range (fun x => g (f x))) :=
by
suffices hg' : BddAbove (g '' range f) by rwa [← Function.comp_def, Set.range_comp]
apply hg.map_bddAbove (by rintro x ⟨a, rfl⟩; exact hf0 a)
obtain ⟨b, hb⟩ := hf
use b, hb
simp only [mem_upperBounds, mem_range, forall_exists_index, forall_apply_eq_imp_iff] at hb
exact le_trans (hf0 Classical.ofNonempty) (hb Classical.ofNonempty)
