English
Let f: β → γ be monotone and γ a ConditionallyCompleteLattice with OrderBot. If g: α → β tends to atBot along a nontrivial filter l, then the infimum of f(g(a)) over a equals the infimum 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
$$$$\inf_{a} f(g(a)) = \inf_{b\in\beta} f(b).$$$$
Lean4
/-- If `f` is a monotone function taking values in a complete lattice
and `g` tends to `atBot` along a nontrivial filter,
then the indexed infimum of `f ∘ g` is equal to the indexed infimum of `f`. -/
theorem _root_.Monotone.iInf_comp_tendsto_atBot [Preorder β] [ConditionallyCompleteLattice γ] [OrderBot γ]
{l : Filter α} [l.NeBot] {f : β → γ} (hf : Monotone f) {g : α → β} (hg : Tendsto g l atBot) :
⨅ a, f (g a) = ⨅ b, f b :=
hf.ciInf_comp_tendsto_atBot (OrderBot.bddBelow _) hg
