measurable_mk

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

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

English

If h is AEMeasurable f μ, then h.mk f is measurable.

Русский

Если h является AE-измеримой f μ, то h.mk f измерима.

LaTeX

$$AEMeasurable f μ ⇒ Measurable (AEMeasurable.mk f h)$$

Lean4

@[measurability]
theorem measurable_mk (h : AEMeasurable f μ) : Measurable (h.mk f) :=
  (Classical.choose_spec h).1

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

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

Разделы

Аффилиация

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