ae_eq_set_symmDiff

Mathlib.MeasureTheory.OuterMeasure.AE

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

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 ae_eq_set_symmDiff {s' t' : Set α} (h : s =ᵐ[μ] t) (h' : s' =ᵐ[μ] t') : s ∆ s' =ᵐ[μ] t ∆ t' :=
  h.symmDiff h'

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

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

Разделы

Аффилиация

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