limsup_const — Mathlib

English

For a constant b and a filter f on α that is nontrivial, the limsup of the constant function equal to b is b.

Русский

Для константы b и фильтра f на α, не равного нижней границе, limsup константной функции равен b.

LaTeX

$$$ \\operatorname{limsup} (\\lambda x. b) \\, f = b $$$

Lean4

@[simp]
theorem limsup_const {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} [NeBot f] (b : β) :
    limsup (fun _ => b) f = b := by simpa only [limsup_eq, eventually_const] using csInf_Ici

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