diff_ae_eq_self

Mathlib.MeasureTheory.OuterMeasure.AE

URI: https://scilib.ai/kg/mathlib#MeasureTheory.diff_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 \setminus s') =ᵐ[\mu] (t \setminus t')$$$

Lean4

theorem diff_ae_eq_self : (s \ t : Set α) =ᵐ[μ] s ↔ μ (s ∩ t) = 0 := by simp [eventuallyLE_antisymm_iff, ae_le_set]

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

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

Разделы

Аффилиация

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