aemeasurable

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

URI: https://scilib.ai/kg/mathlib#Measurable.aemeasurable

English

If f is measurable, then f is AEMeasurable with respect to μ.

Русский

Если функция измерима, то она является AE-измеримой по отношению к μ.

LaTeX

$$Measurable(f) ⇒ AEMeasurable f μ$$

Lean4

@[fun_prop, aesop unsafe 30% apply (rule_sets := [Measurable])]
theorem aemeasurable (h : Measurable f) : AEMeasurable f μ :=
  ⟨f, h, ae_eq_refl f⟩

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

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

Разделы

Аффилиация

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