diff_ae_eq_left

Mathlib.MeasureTheory.Measure.AEDisjoint

URI: https://scilib.ai/kg/mathlib#MeasureTheory.AEDisjoint.diff_ae_eq_left

English

If s is μ-a.e. disjoint from t, then the set difference s \\ t is equal to s almost everywhere with respect to μ.

Русский

Если s почти всюду не пересекается с t по μ, то множество s\\\\t равно s почти по μ.

LaTeX

$$$(s \\\\setminus t) =_{\\\\mu} s$$$

Lean4

theorem diff_ae_eq_left (h : AEDisjoint μ s t) : (s \ t : Set α) =ᵐ[μ] s :=
  @diff_self_inter _ s t ▸ diff_null_ae_eq_self h

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

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

Разделы

Аффилиация

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