English
If f is monotone and g tends to atTop in a linear order, then the indexed supremum of f ∘ g equals the supremum of f, provided the range of f is bounded above.
Русский
Если f монотонна и g стремится к atTop в линейном порядке, то супремум f ∘ g равен супремуму f при условии верхней ограниченности диапазона f.
LaTeX
$$$$\text{Monotone}(f) \rightarrow \operatorname{BddAbove}(\operatorname{range} f) \rightarrow (\operatorname{Tendsto} g\ l\ atTop) \Rightarrow \sup_a f(g(a)) = \sup_b f(b)$$$$
Lean4
/-- If `f` is a monotone function taking values in a conditionally complete linear order
and `g` tends to `atTop` along a nontrivial filter,
then the indexed supremum of `f ∘ g` is equal to the indexed supremum of `f`. -/
theorem _root_.Monotone.ciSup_comp_tendsto_atTop_of_linearOrder [Preorder β] [ConditionallyCompleteLinearOrder γ]
{l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Tendsto g l atTop) :
⨆ a, f (g a) = ⨆ b, f b := by
if hb : BddAbove (range f) then exact hf.ciSup_comp_tendsto_atTop hb hg
else
rw [iSup, iSup, csSup_of_not_bddAbove, csSup_of_not_bddAbove hb]
rwa [BddAbove, ← Function.comp_def f g, hf.upperBounds_range_comp_tendsto_atTop hg]
