English
For HasBasis, limsup equals ciInf of ciSup form, dual to liminf_eq_ciSup_ciInf.
Русский
Для HasBasis лимсуп равен ciInf от ciSup, дуаль к liminf_eq_ciSup_ciInf.
LaTeX
$$limsup f v = ciInf (λ j, ciSup (λ i, f i))$$
Lean4
/-- Writing a limsup as an infimum of supremum, in a (possibly non-complete) conditionally complete
linear order. A reparametrization trick is needed to avoid taking the supremum of sets which are
not bounded above. -/
theorem limsup_eq_ciInf_ciSup {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)]
[Nonempty (Subtype p)] (hv : v.HasBasis p s) {f : ι → α} (hs : ∀ (j : Subtype p), (s j).Nonempty)
(H : ∃ (j : Subtype p), BddAbove (range (fun (i : s j) ↦ f i))) :
limsup f v = ⨅ (j : Subtype p), ⨆ (i : s (limsup_reparam f s p j)), f i :=
HasBasis.liminf_eq_ciSup_ciInf (α := αᵒᵈ) hv hs H
