isGLB_of_tendsto — Mathlib

English

If f is Antitone on s, ha IsLUB s a, hs Nonempty, and hb Tendsto f (nhdsWithin a) (nhds b), then IsGLB (f'' s) b.

Русский

Если f антитонична на s, ha — IsLUB s a, s непусто, и hb стремится к b по nhdsWithin a, тогда IsGLB (f'' s) b.

LaTeX

$$IsLUB.isLUB_of_tendsto (γ := γ^op) hf ha hs hb$$

Lean4

theorem isGLB_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α} {a : α}
    {b : γ} (hf : AntitoneOn f s) (ha : IsLUB s a) (hs : s.Nonempty) (hb : Tendsto f (𝓝[s] a) (𝓝 b)) :
    IsGLB (f '' s) b :=
  IsLUB.isLUB_of_tendsto (γ := γᵒᵈ) hf ha hs hb

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