diff_ae_eq_right

Mathlib.MeasureTheory.Measure.AEDisjoint

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

English

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

Русский

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

LaTeX

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

Lean4

theorem diff_ae_eq_right (h : AEDisjoint μ s t) : (t \ s : Set α) =ᵐ[μ] t :=
  diff_ae_eq_left <| AEDisjoint.symm h

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

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

Разделы

Аффилиация

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