limsup_eq_sInf_iUnion_iInter — Mathlib

English

If v has a basis with p and s, then the limsup of f with respect to v equals the infimum of the union over j of the intersection over i∈s(j) of f(i).

Русский

Если у v есть базис с p и s, то limsup f v = sInf (⋃ j, ⋂ i∈s(j) f(i)).

LaTeX

$$$ \\operatorname{limsup} f v = \\operatorname{sInf}\\Big(\\bigcup_{j} \\bigcap_{i \\in s(j)} f(i)\\Big) $$$

Lean4

theorem limsup_eq_sInf_iUnion_iInter {ι ι' : Type*} {f : ι → α} {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι}
    (hv : v.HasBasis p s) : limsup f v = sInf (⋃ (j : Subtype p), ⋂ (i : s j), Ici (f i)) :=
  HasBasis.liminf_eq_sSup_iUnion_iInter (α := αᵒᵈ) hv

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