English
The almost-everywhere equality holds for the pointwise supremum: (iSup n aeSeq hf p n) =ᵐ (iSup n f n).
Русский
С практически всюду справедимо равенство для точечного верхнего предела: (iSup n aeSeq hf p n) =ᵐ (iSup n f n).
LaTeX
$$$ (iSup\, n, aeSeq\, hf\, p\, n) =^{\mu} (iSup\, n, f\, n) $$$
Lean4
theorem iSup [SupSet β] [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ) (hp : ∀ᵐ x ∂μ, p x fun n => f n x) :
⨆ n, aeSeq hf p n =ᵐ[μ] ⨆ n, f n :=
by
simp_rw [Filter.EventuallyEq, ae_iff, iSup_apply]
have h_ss : aeSeqSet hf p ⊆ {a : α | ⨆ i : ι, aeSeq hf p i a = ⨆ i : ι, f i a} :=
by
intro x hx
congr
exact funext fun i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i
exact measure_mono_null (Set.compl_subset_compl.mpr h_ss) (measure_compl_aeSeqSet_eq_zero hf hp)
