English
For antitone f with bounded range in a linear order, Tendsto g to atTop yields the same infimum for f ∘ g as for f.
Русский
Для антитонной f с ограниченным диапазоном в линейном порядке, при Tendsto g к atTop получаем тот же инфимум для f ∘ g и для f.
LaTeX
$$$$\text{Antitone}(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 `atTop` along a nontrivial filter,
then the indexed infimum of `f ∘ g` is equal to the indexed infimum of `f`.
The assumption `BddBelow (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.ciInf_comp_tendsto_atTop [Preorder β] [ConditionallyCompleteLattice γ] {l : Filter α} [l.NeBot]
{f : β → γ} (hf : Antitone f) (hb : BddBelow (range f)) {g : α → β} (hg : Tendsto g l atTop) :
⨅ a, f (g a) = ⨅ b, f b :=
hf.dual.ciSup_comp_tendsto_atBot hb hg
