ae_eq_mk

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

URI: https://scilib.ai/kg/mathlib#AEMeasurable.ae_eq_mk

English

For any AEMeasurable f μ, f equals h.mk f almost everywhere.

Русский

Для любой AE-измеримой f μ, верно, что f =ᵐ μ h.mk f.

LaTeX

$$f =ᵐ[μ] h.mk f$$

Lean4

theorem ae_eq_mk (h : AEMeasurable f μ) : f =ᵐ[μ] h.mk f :=
  (Classical.choose_spec h).2

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru