isLUB_of_tendsto_atBot — Mathlib

English

If f is monotone and f tends to a along atTop, then IsLUB(range f, a).

Русский

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

LaTeX

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

Lean4

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

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