le_of_tendsto_of_frequently — Mathlib

English

Let f: β → α, a and b in α. If Tendsto f x (nhds a) and f c ≤ b holds frequently along x, then a ≤ b.

Русский

Пусть f: β → α; если f сходится к a по nhds a и f c ≤ b встречается часто, тогда a ≤ b.

LaTeX

$$Tendsto f x (nhds a) ∧ ∃ᶠ c in x, f c ≤ b ⇒ a ≤ b$$

Lean4

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

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