of_discrete

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

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

English

If hf is AEMeasurable f μ and f equals g almost everywhere, then g is AEMeasurable with respect to μ.

Русский

Если hf — AE-измеримая f μ и f =ᵐμ g, то g также AE-измерима по отношению к μ.

LaTeX

$$AEMeasurable f μ ∧ f =ᵐ[μ] g ⇒ AEMeasurable g μ$$

Lean4

theorem of_discrete [DiscreteMeasurableSpace α] : AEMeasurable f μ :=
  Measurable.of_discrete.aemeasurable

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

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

Разделы

Аффилиация

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