English
Let f: β → γ be monotone and let g: α → β be such that g tends to the bottom along a nontrivial filter l. Then the set of lower bounds of the range of f ∘ g is exactly the set of lower bounds of the range of f.
Русский
Пусть f: β → γ монотонна, а g: α → β такова, что g стремится к нижней границе вдоль ненулевого фильтра l. Тогда множество нижних границ диапазона f ∘ g совпадает с множеством нижних границ диапазона f.
LaTeX
$$$\operatorname{LowerBounds}\big(\operatorname{range}(f \circ g)\big) = \operatorname{LowerBounds}\big(\operatorname{range}(f)\big)$$$
Lean4
/-- If `f` is a monotone function and `g` tends to `atBot` along a nontrivial filter.
then the lower bounds of the range of `f ∘ g`
are the same as the lower bounds of the range of `f`. -/
theorem _root_.Monotone.lowerBounds_range_comp_tendsto_atBot [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot]
{f : β → γ} (hf : Monotone f) {g : α → β} (hg : Tendsto g l atBot) :
lowerBounds (range (f ∘ g)) = lowerBounds (range f) :=
hf.dual.upperBounds_range_comp_tendsto_atTop hg
