isGLB_of_tendsto — Mathlib

English

In a dual ordered setting, if f is monotone on s and a is the LUB of s with Tendsto to b, then IsLUB (f'' s) b.

Русский

В дуальном порядке, если f монотонна на s и a является ЛУБ s с пределом к b, то IsLUB (f'' s) b.

LaTeX

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

Lean4

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

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