le_of_tendsto — Mathlib

English

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

Русский

Пусть f: β → α и a,b ∈ α. Если Tendsto f x (nhds a) и f c ≤ b выполняется eventually в x, тогда a ≤ b.

LaTeX

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

Lean4

theorem le_of_tendsto {x : Filter β} [NeBot x] (lim : Tendsto f x (𝓝 a)) (h : ∀ᶠ c in x, f c ≤ b) : a ≤ b :=
  isClosed_Iic.mem_of_tendsto lim h

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