isLUB_of_tendsto — Mathlib

English

If f is AntitoneOn on s and a is GLB s a, s nonempty, and Tendsto f (nhdsWithin a s) (nhds b), then IsGLB (f'' s) b.

Русский

Если f антитонична на s и a является GLB s, s непусто, и Tendsto f (nhdsWithin a s) (nhds b), тогда IsGLB (f'' s) b.

LaTeX

$$IsGLB.isGLB_of_tendsto (γ := γᵒᵈ) hf ha hs hb$$

Lean4

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

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