le_of_tendsto — Mathlib

English

If f is antitone and Tendsto to a, then f(b) ≥ a for all b.

Русский

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

LaTeX

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

Lean4

theorem le_of_tendsto [TopologicalSpace α] [Preorder α] [OrderClosedTopology α] [SemilatticeSup β] {f : β → α} {a : α}
    (hf : Antitone f) (ha : Tendsto f atTop (𝓝 a)) (b : β) : a ≤ f b :=
  hf.dual_right.ge_of_tendsto ha b

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