English
In a suitable ordered setting, limsup of a function equals bottom if and only if the function is eventually constantly bottom.
Русский
В подходящем упорядоченном окружении limsup функции равен нулю/нижнему пределу тогда и только тогда, когда функция в конечном счете постоянно равна нулю.
LaTeX
$$$ (f : Filter β) [CountableInterFilter f] [CompleteLinearOrder α] [TopologicalSpace α] [FirstCountableTopology α] [OrderTopology α] \Rightarrow (\limsup u f = \bot) \Leftrightarrow (u =^f \bot). $$$
Lean4
@[simp]
theorem limsup_eq_bot : f.limsup u = ⊥ ↔ u =ᶠ[f] ⊥ :=
⟨fun h =>
(EventuallyLE.trans eventually_le_limsup <| Eventually.of_forall fun _ => h.le).mono fun _ hx =>
le_antisymm hx bot_le,
fun h => by
rw [limsup_congr h]
exact limsup_const_bot⟩
