mem_upperBounds_of_tendsto — Mathlib

English

Under dual order, if hf is antisymmetric, and ha is IsLUB s a, hs Nonempty, hb Tendsto f (nhdsWithin a) (nhds b), then IsLUB (f'' s) b.

Русский

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

LaTeX

$$IsLUB.isLUB_of_tendsto (α := αᵒᵈ) (γ := γᵒᵈ) hf ha hs hb$$

Lean4

theorem mem_upperBounds_of_tendsto [Preorder γ] [TopologicalSpace γ] [OrderClosedTopology γ] {f : α → γ} {s : Set α}
    {a : α} {b : γ} (hf : AntitoneOn f s) (ha : IsGLB s a) (hb : Tendsto f (𝓝[s] a) (𝓝 b)) : b ∈ upperBounds (f '' s) :=
  IsGLB.mem_lowerBounds_of_tendsto (γ := γᵒᵈ) hf ha hb

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