English
If f is monotone and g tends to atTop, the upper bounds of the range of f ∘ g equal the upper bounds of the range of f.
Русский
Если f монотонна и g стремится к верхнему пределу, то верхние границы диапазона f ∘ g совпадают с верхними границами диапазона f.
LaTeX
$$$$ \operatorname{upperBounds}(\operatorname{range}(f \circ g)) = \operatorname{upperBounds}(\operatorname{range}(f)). $$$$
Lean4
/-- If `f` is a monotone function and `g` tends to `atTop` along a nontrivial filter.
then the upper bounds of the range of `f ∘ g`
are the same as the upper bounds of the range of `f`.
This lemma together with `exists_seq_monotone_tendsto_atTop_atTop` below
is useful to reduce a statement
about a monotone family indexed by a type with countably generated `atTop` (e.g., `ℝ`)
to the case of a family indexed by natural numbers. -/
theorem _root_.Monotone.upperBounds_range_comp_tendsto_atTop [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot]
{f : β → γ} (hf : Monotone f) {g : α → β} (hg : Tendsto g l atTop) :
upperBounds (range (f ∘ g)) = upperBounds (range f) :=
by
refine Subset.antisymm ?_ (upperBounds_mono_set <| range_comp_subset_range _ _)
rintro c hc _ ⟨b, rfl⟩
obtain ⟨a, ha⟩ : ∃ a, b ≤ g a := (hg.eventually_ge_atTop b).exists
exact (hf ha).trans <| hc <| mem_range_self _
