English
Let f: β → γ be an antitone function and let g: α → β tend to the bottom along a nontrivial filter l, where β is preordered and γ is a ConditionallyCompleteLinearOrder with a bottom. Then the supremum of the composite f ∘ g is the same as the supremum of f over β; i.e., ⨆ a, f(g(a)) = ⨆ b, f(b).
Русский
Пусть f: β → γ антимонотна и пусть g: α → β стремится к нижней границе вдоль ненулевого фильтра l, где β упорядочено и γ является условно полноупорядоченной линейной множеством с нижней границей. Тогда супремум композиции f ∘ g равен супремуму f по β; то есть ⨆ a, f(g(a)) = ⨆ b, f(b).
LaTeX
$$$$\sup_{a} f(g(a)) = \sup_{b\in\beta} f(b).$$$$
Lean4
/-- If `f` is an antitone function taking values in a conditionally complete linear order
and `g` tends to `atBot` along a nontrivial filter,
then the indexed supremum of `f ∘ g` is equal to the indexed supremum of `f`. -/
theorem _root_.Antitone.ciSup_comp_tendsto_atBot_of_linearOrder [Preorder β] [ConditionallyCompleteLinearOrder γ]
{l : Filter α} [l.NeBot] {f : β → γ} (hf : Antitone f) {g : α → β} (hg : Tendsto g l atBot) :
⨆ a, f (g a) = ⨆ b, f b :=
hf.dual_left.ciSup_comp_tendsto_atTop_of_linearOrder hg
