aeSeq_eq_fun_ae — Mathlib

English

There holds ∀ᵐ a ∂μ, ∀ i, aeSeq hf p i a = f i a.

Русский

Пусть ∀ᵐ a ∂μ, ∀ i, aeSeq hf p i a = f i a.

LaTeX

$$$ ∀^\! a \partial\mu,\ ∀ i,\ aeSeq\, hf\, p\, i\, a = f i a $$$

Lean4

theorem aeSeq_eq_fun_ae [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ) (hp : ∀ᵐ x ∂μ, p x fun n => f n x) :
    ∀ᵐ a : α ∂μ, ∀ i : ι, aeSeq hf p i a = f i a :=
  haveI h_ss : {a : α | ¬∀ i : ι, aeSeq hf p i a = f i a} ⊆ (aeSeqSet hf p)ᶜ := fun _ =>
    mt fun hx i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i
  measure_mono_null h_ss (measure_compl_aeSeqSet_eq_zero hf hp)

Похожие утверждения