English
If f is monotone with bounded range and g tends to atTop along a nontrivial filter, then the indexed supremum of f ∘ g equals the supremum of f.
Русский
Если f монотонна с ограниченным диапазоном и g стремится к atTop вдоль ненулевого фильтра, то инфимум верхний для f ∘ g равен инфимум верхний для f.
LaTeX
$$$$\text{Monotone}(f) \rightarrow \operatorname{BddAbove}(\operatorname{range} f) \rightarrow (\operatorname{Tendsto} g\ l\ atTop) \\Rightarrow \operatorname{iSup}(a \mapsto f(g(a))) = \operatorname{iSup}(b \mapsto f(b))$$$$
Lean4
/-- If `f` is a monotone function taking values in a conditionally complete linear order
and `g` tends to `atBot` along a nontrivial filter,
then the indexed infimum of `f ∘ g` is equal to the indexed infimum of `f`. -/
theorem _root_.Monotone.ciInf_comp_tendsto_atBot_of_linearOrder [Preorder β] [ConditionallyCompleteLinearOrder γ]
{l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Tendsto g l atBot) :
⨅ a, f (g a) = ⨅ b, f b :=
hf.dual.ciSup_comp_tendsto_atTop_of_linearOrder hg
