ae_mem_imp_eq_mk — Mathlib

English

If h is AEMeasurable f on μ restricted to s, then μ-almost every x in s satisfies f(x) = h.mk f x.

Русский

Если h является AEMeasurable f относительно μ ограниченного до s, то μ-почти во всех x из s выполняется f(x) = h.mk f x.

LaTeX

$$$\\\\forall_{\\\\mu} x, x \\\\in s \\\\Rightarrow f x = h.mk f x \\\\text{ for μ-a.e. } x$$$

Lean4

theorem ae_mem_imp_eq_mk {s} (h : AEMeasurable f (μ.restrict s)) : ∀ᵐ x ∂μ, x ∈ s → f x = h.mk f x :=
  ae_imp_of_ae_restrict h.ae_eq_mk

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