diff_null_ae_eq_self

Mathlib.MeasureTheory.OuterMeasure.AE

URI: https://scilib.ai/kg/mathlib#MeasureTheory.diff_null_ae_eq_self

English

If s =ᵐ t and s' =ᵐ t' then s ∆ s' =ᵐ t ∆ t'.

Русский

Если s =ᵐ t и s' =ᵐ t', то s ∆ s' =ᵐ t ∆ t'.

LaTeX

$$$(s =ᵐ[\mu] t) \Rightarrow (s' =ᵐ[\mu] t') \Rightarrow (s \Delta s') =ᵐ[\mu] (t \Delta t')$$$

Lean4

theorem diff_null_ae_eq_self (ht : μ t = 0) : (s \ t : Set α) =ᵐ[μ] s :=
  diff_ae_eq_self.mpr (measure_mono_null inter_subset_right ht)

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

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

Разделы

Аффилиация

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