English
In a linear order, for monotone f, the above equality holds with Tendsto g to atTop, provided the same boundedness assumption.
Русский
В линейном порядке при монотонной f равенство выполняется при Tendsto g к atTop и при условии той же ограниченности.
LaTeX
$$$$\text{Monotone}(f)\rightarrow \operatorname{BddAbove}(\operatorname{range} f) \rightarrow (\operatorname{Tendsto} g\ l\ atTop) \Rightarrow \inf_a f(g(a)) = \inf_b f(b)$$$$
Lean4
/-- If `f` is an antitone function with bounded range
and `g` tends to `atBot` 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_.Antitone.ciSup_comp_tendsto_atBot [Preorder β] [ConditionallyCompleteLattice γ] {l : Filter α} [l.NeBot]
{f : β → γ} (hf : Antitone f) (hb : BddAbove (range f)) {g : α → β} (hg : Tendsto g l atBot) :
⨆ a, f (g a) = ⨆ b, f b :=
hf.dual_left.ciSup_comp_tendsto_atTop hb hg
