range_of_tendsto — Mathlib

English

Let f: β → α and F a filter with F.NeBot. If ∀ i, f(i) ≤ a and Tendsto f F (nhds a), then IsLUB(range f) a.

Русский

Пусть f: β → α и F — фильтр, F.NeBot. Если ∀ i, f(i) ≤ a и Tendsto f F (nhds a), то IsLUB(range f) a.

LaTeX

$$IsLUB(range f) a$$

Lean4

theorem range_of_tendsto {F : Filter β} [F.NeBot] (hle : ∀ i, f i ≤ a) (hlim : Tendsto f F (𝓝 a)) : IsLUB (range f) a :=
  ⟨forall_mem_range.mpr hle, fun _c hc ↦ le_of_tendsto' hlim fun i ↦ hc <| mem_range_self i⟩

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