English
If the symmetric difference of u and v is null when restricted to w, then s(w ∩ u) = s(w ∩ v).
Русский
Если симметрическая разность u и v нулевая на w, то мера s на пересечении w с u равна мере на пересечении w с v.
LaTeX
$$$$ (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w) (hsu : 0 ≤[u] s) (hsv : 0 ≤[v] s) (hs : s (u \Delta v) = 0) : s (w \cap u) = s (w \cap v). $$$$
Lean4
theorem of_inter_eq_of_symmDiff_eq_zero_positive (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w)
(hsu : 0 ≤[u] s) (hsv : 0 ≤[v] s) (hs : s (u ∆ v) = 0) : s (w ∩ u) = s (w ∩ v) :=
by
have hwuv : s ((w ∩ u) ∆ (w ∩ v)) = 0 :=
by
refine
subset_positive_null_set (hu.union hv) ((hw.inter hu).symmDiff (hw.inter hv)) (hu.symmDiff hv)
(restrict_le_restrict_union _ _ hu hsu hv hsv) hs Set.symmDiff_subset_union ?_
rw [← Set.inter_symmDiff_distrib_left]
exact Set.inter_subset_right
obtain ⟨huv, hvu⟩ :=
of_diff_eq_zero_of_symmDiff_eq_zero_positive (hw.inter hu) (hw.inter hv)
(restrict_le_restrict_subset _ _ hu hsu (w.inter_subset_right))
(restrict_le_restrict_subset _ _ hv hsv (w.inter_subset_right)) hwuv
rw [← of_diff_of_diff_eq_zero (hw.inter hu) (hw.inter hv) hvu, huv, zero_add]
