English
Let f: β → γ be antitone and let g: α → β tend to atTop along a nontrivial filter l. Then the lower bounds of the range of f ∘ g equal the lower bounds of the range of f.
Русский
Пусть f: β → γ антимонотонна и 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 an antitone function and `g` tends to `atTop` 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.lowerBounds_range_comp_tendsto_atTop [Preorder β] [Preorder γ] {l : Filter α} [l.NeBot]
{f : β → γ} (hf : Antitone f) {g : α → β} (hg : Tendsto g l atTop) :
lowerBounds (range (f ∘ g)) = lowerBounds (range f) :=
hf.dual_left.lowerBounds_range_comp_tendsto_atBot hg
