ge_of_tendsto_of_frequently — Mathlib

English

If f tends to a along x and f is frequently bounded below by b, then b ≤ a.

Русский

Если f сходится к a вдоль фильтра x и часто выполняется неравенство b ≤ f c, то b ≤ a.

LaTeX

$$$ \text{Tendsto } f\ x\ (\mathcal{N} a) \\Rightarrow\\ Frequently\ (\lambda c, b \le f c)\ x \\Rightarrow\\ b \le a $$$

Lean4

theorem ge_of_tendsto_of_frequently {x : Filter β} (lim : Tendsto f x (𝓝 a)) (h : ∃ᶠ c in x, b ≤ f c) : b ≤ a :=
  isClosed_Ici.mem_of_frequently_of_tendsto h lim

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