English
Let f: β → γ be antitone and g: α → β tend to atBot along a nontrivial filter l. Then the upper bounds of the range of f ∘ g coincide with the upper bounds of the range of f.
Русский
Пусть f: β → γ антимонотонна и g: α → β стремится к нижней границе вдоль ненулевого фильтра l. Тогда верхние границы диапазона f ∘ g совпадают с верхними границами диапазона f.
LaTeX
$$$\operatorname{UpperBounds}\big(\operatorname{range}(f \circ g)\big) = \operatorname{UpperBounds}\big(\operatorname{range}(f)\big)$$$
Lean4
/-- If `f` is an antitone function and `g` tends to `atBot` along a nontrivial filter.
then the upper bounds of the range of `f ∘ g`
are the same as the upper bounds of the range of `f`. -/
theorem _root_.Antitone.upperBounds_range_comp_tendsto_atBot [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot]
{f : β → γ} (hf : Antitone f) {g : α → β} (hg : Tendsto g l atBot) :
upperBounds (range (f ∘ g)) = upperBounds (range f) :=
hf.dual.lowerBounds_range_comp_tendsto_atTop hg
