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