English
Let f: β → γ be monotone and γ be a ConditionallyCompleteLattice with OrderTop. If g: α → β tends to atTop along a nontrivial filter l, then the supremum of f(g(a)) over a equals the supremum of f over β; i.e., ⨆ a, f(g(a)) = ⨆ b, f(b).
Русский
Пусть f: β → γ монотонна и γ — условно полноупорядоченная решётка с верхней границей. Пусть g: α → β стремится к верхней границе вдоль ненулевого фильтра l. Тогда супремум f(g(a)) по a равен супремуму f по β; то есть ⨆ a, f(g(a)) = ⨆ b, f(b).
LaTeX
$$$$\sup_{a} f(g(a)) = \sup_{b\in\beta} f(b).$$$$
Lean4
/-- If `f` is a monotone function taking values in a complete lattice
and `g` tends to `atTop` along a nontrivial filter,
then the indexed supremum of `f ∘ g` is equal to the indexed supremum of `f`. -/
theorem _root_.Monotone.iSup_comp_tendsto_atTop [Preorder β] [ConditionallyCompleteLattice γ] [OrderTop γ]
{l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Tendsto g l atTop) :
⨆ a, f (g a) = ⨆ b, f b :=
hf.ciSup_comp_tendsto_atTop (OrderTop.bddAbove _) hg
