ae_eq

Mathlib.MeasureTheory.Measure.AbsolutelyContinuous

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.AbsolutelyContinuous.ae_eq

English

If μ ≪ ν and f and g are equal almost everywhere with respect to ν, then f and g are equal almost everywhere with respect to μ.

Русский

Если μ ≪ ν и f =ᵐ[ν] g, то f =ᵐ[μ] g.

LaTeX

$$μ ≪ ν ∧ (f =ᵐ[ν] g) → (f =ᵐ[μ] g)$$

Lean4

theorem ae_eq (h : μ ≪ ν) {f g : α → δ} (h' : f =ᵐ[ν] g) : f =ᵐ[μ] g :=
  h.ae_le h'

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

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

Разделы

Аффилиация

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