English
If the symmetric difference of two positive sets is measure-zero, then the differences between the two sets also have zero s-measure.
Русский
Если симметрическая разность двух положительных множеств имеет нулевую меру, то и их различия имеют нулевую меру по s.
LaTeX
$$$$ (hu : MeasurableSet u)\; (hv : MeasurableSet v)\; (hsu : s ≤[u] 0)\; (hsv : s ≤[v] 0)\; (hs : s (u \Delta v) = 0) \Rightarrow\; s (u \setminus v) = 0 \land s (v \setminus u) = 0. $$$$
Lean4
/-- If the symmetric difference of two positive sets is a null-set, then so are the differences
between the two sets. -/
theorem of_diff_eq_zero_of_symmDiff_eq_zero_positive (hu : MeasurableSet u) (hv : MeasurableSet v) (hsu : 0 ≤[u] s)
(hsv : 0 ≤[v] s) (hs : s (u ∆ v) = 0) : s (u \ v) = 0 ∧ s (v \ u) = 0 :=
by
rw [restrict_le_restrict_iff] at hsu hsv
on_goal 1 =>
have a := hsu (hu.diff hv) diff_subset
have b := hsv (hv.diff hu) diff_subset
rw [Set.symmDiff_def,
of_union (v := s) (Set.disjoint_of_subset_left diff_subset disjoint_sdiff_self_right) (hu.diff hv)
(hv.diff hu)] at hs
rw [zero_apply] at a b
constructor
all_goals
first
| linarith
| assumption
