English
If s is countable and each f_i is AEMeasurable, then the a.e. measurable infimum over i∈s is AEMeasurable.
Русский
Если f_i — AEMeasurable, то инфимум по i∈s — AEMeasurable.
LaTeX
$$theorem AEMeasurable.biInf {ι} {μ : Measure δ} (s : Set ι) {f : ι → δ → α} (hs : s.Countable) (hf : ∀ i ∈ s, AEMeasurable (f i) μ) : AEMeasurable (fun b => iInf fun i => iInf fun h => f i b) μ$$
Lean4
/-- `limsup` over a general filter is measurable. See `Measurable.limsup` for the version over `ℕ`.
-/
theorem limsup' {ι ι'} {f : ι → δ → α} {u : Filter ι} (hf : ∀ i, Measurable (f i)) {p : ι' → Prop} {s : ι' → Set ι}
(hu : u.HasCountableBasis p s) (hs : ∀ i, (s i).Countable) : Measurable fun x => limsup (fun i => f i x) u :=
.liminf' (α := αᵒᵈ) hf hu hs
