mem_lowerBounds_of_tendsto — Mathlib

English

If f is Antitone on s, a is IsLUB s a, and f tends to b along nhdsWithin a s, then b is a lower bound of f(s).

Русский

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

LaTeX

$$AntitoneOn f s → IsLUB s a → Tendsto f (nhdsWithin a s) (nhds b) → b ∈ lowerBounds (Set.image f s)$$

Lean4

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

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