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