English
Reductive form of limsup via HasBasis with ITE blocks.
Русский
Уменьшенная форма лимсупа через HasBasis с блоками ITE.
LaTeX
$$limsup f v = ite (Exists j, s j = ∅) (sInf univ) (ite (∀ j, ¬BddBelow (range (i ↦ f i))) (sInf ∅) (⨅ j, ⨆ 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 below. -/
theorem limsup_eq_ite {v : Filter ι} {p : ι' → Prop} {s : ι' → Set ι} [Countable (Subtype p)] [Nonempty (Subtype p)]
(hv : v.HasBasis p s) (f : ι → α) :
limsup f v =
if ∃ (j : Subtype p), s j = ∅ then sInf univ
else
if ∀ (j : Subtype p), ¬BddAbove (range (fun (i : s j) ↦ f i)) then sInf ∅
else ⨅ (j : Subtype p), ⨆ (i : s (limsup_reparam f s p j)), f i :=
HasBasis.liminf_eq_ite (α := αᵒᵈ) hv f
