liminf_const — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem liminf_const {α : Type*} [ConditionallyCompleteLattice β] {f : Filter α} [NeBot f] (b : β) :
    liminf (fun _ => b) f = b :=
  limsup_const (β := βᵒᵈ) b

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