mem_lowerBounds_of_tendsto — Mathlib

English

If a is the LUB of s, s is nonempty, and f tends to b along nhdsWithin a s, then IsLUB (f'' s) b.

Русский

Если a — наибольшая верхняя граница множества s, s непусто, и f стремится к b по nhdsWithin a s, тогда IsLUB (f'' s) b.

LaTeX

$$MonotoneOn f s → IsLUB s a → s.Nonempty → Tendsto f (nhdsWithin a s) (nhds b) → IsLUB (Set.image f s) b$$

Lean4

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

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