indicator_ae_eq_of_ae_eq_set

Mathlib.MeasureTheory.Measure.Restrict

URI: https://scilib.ai/kg/mathlib#indicator_ae_eq_of_ae_eq_set

English

If s =ᵐ[μ] t then s.indicator f =ᵐ[μ] t.indicator f.

Русский

Если s и t равны почти повсюду по μ, то sf = tf почти наверху по μ.

LaTeX

$$$ (s =^{\\mathrm{ae}}_{\\mu} t) \\Rightarrow s.indicator f =^{\\mathrm{ae}}_{\\mu} t.indicator f $$$

Lean4

theorem indicator_ae_eq_of_ae_eq_set (hst : s =ᵐ[μ] t) : s.indicator f =ᵐ[μ] t.indicator f := by
  classical exact piecewise_ae_eq_of_ae_eq_set hst

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

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

Разделы

Аффилиация

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