English
Let f: β → γ be antitone and γ a ConditionallyCompleteLattice with OrderTop. If g: α → β tends to atBot along a nontrivial filter l, then the supremum of f(g(a)) equals the supremum of f over β; i.e., ⨆ a, f(g(a)) = ⨆ b, f(b).
Русский
Пусть f: β → γ антимонотна и γ — условно полноупорядоченная решётка с верхней границей. Пусть g: α → β стремится к нижней границе вдоль ненулевого фильтра l. Тогда верхняя граница значений f(g(a)) равна верхней границе значений f(b) по b; то есть ⨆ 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 complete lattice
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.iSup_comp_tendsto_atBot [Preorder β] [ConditionallyCompleteLattice γ] [OrderTop γ]
{l : Filter α} [l.NeBot] {f : β → γ} (hf : Antitone f) {g : α → β} (hg : Tendsto g l atBot) :
⨆ a, f (g a) = ⨆ b, f b :=
hf.ciSup_comp_tendsto_atBot (OrderTop.bddAbove _) hg
