English
If NoMinOrder β and Tendsto f l atBot, then range f is not bounded below.
Русский
Если у β нет минимума (NoMinOrder) и Tendsto f l к atBot, тогда range f не ограничен снизу.
LaTeX
$$$$[NoMinOrder(\beta)](\operatorname{Tendsto} f\ l\ \text{atBot}) \Rightarrow \neg \operatorname{BddBelow}(\operatorname{range} f)$$$$
Lean4
/-- If `f` is a monotone function with bounded range
and `g` tends to `atTop` along a nontrivial filter,
then the indexed supremum of `f ∘ g` is equal to the indexed supremum of `f`.
The assumption `BddAbove (range f)` can be omitted,
if the codomain of `f` is a conditionally complete linear order or a complete lattice, see below.
-/
theorem _root_.Monotone.ciSup_comp_tendsto_atTop [Preorder β] [ConditionallyCompleteLattice γ] {l : Filter α} [l.NeBot]
{f : β → γ} (hf : Monotone f) (hb : BddAbove (range f)) {g : α → β} (hg : Tendsto g l atTop) :
⨆ a, f (g a) = ⨆ b, f b := by
have : Nonempty α := nonempty_of_neBot l
have : Nonempty β := .map g ‹_›
rw [← csInf_upperBounds_range, ← csInf_upperBounds_range, ← hf.upperBounds_range_comp_tendsto_atTop hg,
Function.comp_def]
exacts [hb, hb.mono <| range_comp_subset_range _ _]
