English
A form of liminf as an ite-expression involving HasBasis; reduces to the ciSup/ciInf form.
Русский
Форма лиминфа через ITE с HasBasis; сводится к ciSup/ciInf.
LaTeX
$$liminf f v = ite (Exists j, s j = ∅) sSup univ (ite (∀ j, ¬BddBelow (range (i ↦ f i))) sSup ∅ (⨆ j, ⨅ i, f i))$$
Lean4
/-- Given an indexed family of sets `s j` and a function `f`, then `limsup_reparam j` is equal
to `j` if `f` is bounded above on `s j`, and otherwise to some index `k` such that `f` is bounded
above on `s k` (if there exists one). To ensure good measurability behavior, this index `k` is
chosen as the minimal suitable index. This function is used to write down a limsup in a measurable
way, in `Filter.HasBasis.limsup_eq_ciInf_ciSup` and `Filter.HasBasis.limsup_eq_ite`. -/
noncomputable def limsup_reparam (f : ι → α) (s : ι' → Set ι) (p : ι' → Prop) [Countable (Subtype p)]
[Nonempty (Subtype p)] (j : Subtype p) : Subtype p :=
liminf_reparam (α := αᵒᵈ) f s p j
