limsInf_eq_iSup_sInf — Mathlib

English

If f has a basis p,s, then limsInf f equals the supremum over i with p(i) of sInf(s(i)).

Русский

Если у фильтра f имеется базис p,s, тогда лиминф f равен супремуму по i с условием p(i) от sInf(s(i)).

LaTeX

$$$\\operatorname{limsInf} f = \\bigvee_{i} \\bigvee_{(h: p(i))} \\operatorname{sInf}(s(i))$$$

Lean4

theorem limsInf_eq_iSup_sInf {p : ι → Prop} {s : ι → Set α} {f : Filter α} (h : f.HasBasis p s) :
    limsInf f = ⨆ (i) (_ : p i), sInf (s i) :=
  HasBasis.limsSup_eq_iInf_sSup (α := αᵒᵈ) h

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