liminf_eq_sSup_sInf — Mathlib

English

For a filter F on ι and a map a : ι → R, with R a complete lattice, liminf a F equals the supremum over I ∈ F.sets of the infimum over a(I).

Русский

Для фильтра F на ι и отображения a : ι → R, где R — полная решетка, liminf a F = sup_{I∈F.sets} inf a(I).

LaTeX

$$$\\displaystyle \\liminf a F = \\sup\\{ \\inf(a''I) : I \\in F.sets \\}$$$

Lean4

theorem liminf_eq_sSup_sInf {ι R : Type*} (F : Filter ι) [CompleteLattice R] (a : ι → R) :
    liminf a F = sSup ((fun I => sInf (a '' I)) '' F.sets) :=
  @Filter.limsup_eq_sInf_sSup ι (OrderDual R) _ _ a

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