congr

Mathlib.MeasureTheory.Measure.MeasureSpaceDef

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

English

If hf is AEMeasurable f μ and h: f =ᵐ μ g, then AEMeasurable g μ.

Русский

Если hf — AE-измеримая f μ и f =ᵐ μ g, то AEMeasurable g μ.

LaTeX

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

Lean4

theorem congr (hf : AEMeasurable f μ) (h : f =ᵐ[μ] g) : AEMeasurable g μ :=
  ⟨hf.mk f, hf.measurable_mk, h.symm.trans hf.ae_eq_mk⟩

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

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

Разделы

Аффилиация

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