isGLB_of_tendsto_atBot — Mathlib

English

If f is monotone and Tendsto to a along atBot, then a is the greatest lower bound of the range of f.

Русский

Если f монотонна и стремится к a по atBot, то a является наибольшей нижней границей образа f.

LaTeX

$$$ \text{Monotone}(f) \wedge \operatorname{Tendsto} f \operatorname{atBot} (\nhds a) \Rightarrow IsGLB(\operatorname{range} f, a) $$$

Lean4

theorem isGLB_of_tendsto_atBot [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Nonempty β] [SemilatticeInf β]
    {f : β → α} {a : α} (hf : Monotone f) (ha : Tendsto f atBot (𝓝 a)) : IsGLB (Set.range f) a :=
  @isLUB_of_tendsto_atTop αᵒᵈ βᵒᵈ _ _ _ _ _ _ _ hf.dual ha

Похожие утверждения