isGLB_of_tendsto_atTop — Mathlib

English

If f is antitone and f tends to a along atTop, then IsGLB(range f, a).

Русский

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

LaTeX

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

Lean4

theorem isGLB_of_tendsto_atTop [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [Nonempty β] [SemilatticeSup β]
    {f : β → α} {a : α} (hf : Antitone f) (ha : Tendsto f atTop (𝓝 a)) : IsGLB (Set.range f) a :=
  @isGLB_of_tendsto_atBot α βᵒᵈ _ _ _ _ _ _ _ hf.dual_left ha

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