ae_mem_imp_eq_mk — Mathlib

English

If f is AEStronglyMeasurable on μ.restrict s, then almost every x in s satisfies f x = hf.mk f x for the witness hf.

Русский

Если f AE‑строго измерима по μ.restrict s, то почти во всех x в s выполняется f x = hf.mk f x для свидетеля hf.

LaTeX

$$$\\text{Ae condition on }s: \\; \\forall^* x\\, (x \\in s \\Rightarrow f(x) = hf.mk f(x))$$$

Lean4

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

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