aeSeq_n_eq_fun_n_ae — Mathlib

English

For Countable ι, hf and hp, for each fixed n we have aeSeq hf p n =ᵐ f n.

Русский

Для счетного ι, hf и hp, для каждого фиксированного n выполняется aeSeq hf p n =ᵐ f n.

LaTeX

$$$ aeSeq\, hf\, p\, n =\!\!\mu\, f n $ для всех n.$$

Lean4

theorem aeSeq_n_eq_fun_n_ae [Countable ι] (hf : ∀ i, AEMeasurable (f i) μ) (hp : ∀ᵐ x ∂μ, p x fun n => f n x) (n : ι) :
    aeSeq hf p n =ᵐ[μ] f n :=
  ae_all_iff.mp (aeSeq_eq_fun_ae hf hp) n

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