ge_of_tendsto — Mathlib

English

If f is monotone and Tendsto to a, then f(b) ≥ a for all b in the domain under suitable topological assumptions.

Русский

Если f монотонна и стремится к a, тогда f(b) ≥ a для всех b при подходящих условиях топологии.

LaTeX

$$$ \text{Monotone}(f) \wedge \operatorname{Tendsto} f \operatorname{atTop} (\nhds a) \Rightarrow f(b) \ge a $$$

Lean4

theorem ge_of_tendsto [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [SemilatticeSup β] {f : β → α} {a : α}
    (hf : Monotone f) (ha : Tendsto f atTop (𝓝 a)) (b : β) : f b ≤ a :=
  haveI : Nonempty β := Nonempty.intro b
  _root_.ge_of_tendsto ha ((eventually_ge_atTop b).mono fun _ hxy => hf hxy)

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