English
If f is monotone and has a bounded above range, and g tends to atTop along a nontrivial filter, then the indexed infimum of f ∘ g equals the infimum of f.
Русский
Если f монотонна и имеет верхнюю границу диапазона, а g стремится к atTop вдоль ненулевого фильтра, то инфимум по f∘g равен инфимума по f.
LaTeX
$$$$\text{Monotone}(f) \rightarrow \operatorname{BddAbove}(\operatorname{range} f) \rightarrow (\operatorname{Tendsto} g\ l\ \text{atTop}) \Rightarrow \inf_a f(g(a)) = \inf_b f(b)$$$$
Lean4
/-- If `f` is a monotone function with bounded range
and `g` tends to `atBot` 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_.Monotone.ciInf_comp_tendsto_atBot [Preorder β] [ConditionallyCompleteLattice γ] {l : Filter α} [l.NeBot]
{f : β → γ} (hf : Monotone f) (hb : BddBelow (range f)) {g : α → β} (hg : Tendsto g l atBot) :
⨅ a, f (g a) = ⨅ b, f b :=
hf.dual.ciSup_comp_tendsto_atTop hb hg
