limsup_eq — Mathlib

English

If a function has a limit along a filter, then its limsup equals that limit.

Русский

Если функция имеет предел вдоль фильтра, то её limsup равен этому пределу.

LaTeX

$$$ {f}\; {\to}\; {a} \Rightarrow \ limsup\; u\; f = a. $$$

Lean4

/-- If a function has a limit, then its limsup coincides with its limit. -/
theorem limsup_eq {f : Filter β} {u : β → α} {a : α} [NeBot f] (h : Tendsto u f (𝓝 a)) : limsup u f = a :=
  limsSup_eq_of_le_nhds h

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