English
If s is countable and each f_i is measurable, then the function b ↦ iInf i∈s f_i(b) is measurable.
Русский
Если s счетно и каждая f_i измерима, то инфимум по i∈s f_i(b) измерим.
LaTeX
$$s.Countable → (∀ i, Measurable (f i)) → Measurable fun b => iInf fun i => iInf fun h => f i b$$
Lean4
theorem biSup {ι} (s : Set ι) {f : ι → δ → α} (hs : s.Countable) (hf : ∀ i ∈ s, Measurable (f i)) :
Measurable fun b => ⨆ i ∈ s, f i b :=
by
haveI : Encodable s := hs.toEncodable
by_cases H : ∀ i, i ∈ s
· have : ∀ b, ⨆ i ∈ s, f i b = ⨆ (i : s), f i b := fun b ↦ cbiSup_eq_of_forall (f := fun i ↦ f i b) H
simp only [this]
exact .iSup (fun (i : s) ↦ hf i i.2)
· have : ∀ b, ⨆ i ∈ s, f i b = (⨆ (i : s), f i b) ⊔ sSup ∅ := fun b ↦ cbiSup_eq_of_not_forall (f := fun i ↦ f i b) H
simp only [this]
apply Measurable.sup _ measurable_const
exact .iSup (fun (i : s) ↦ hf i i.2)
