of_diff_eq_zero_of_symmDiff_eq_zero_negative

English

If the symmetric difference of two negative sets is measure-zero, then the differences between the two sets 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) : s (u \setminus v) = 0 \land s (v \setminus u) = 0. $$$$

Lean4

/-- If the symmetric difference of two negative sets is a null-set, then so are the differences
between the two sets. -/
theorem of_diff_eq_zero_of_symmDiff_eq_zero_negative (hu : MeasurableSet u) (hv : MeasurableSet v) (hsu : s ≤[u] 0)
    (hsv : s ≤[v] 0) (hs : s (u ∆ v) = 0) : s (u \ v) = 0 ∧ s (v \ u) = 0 :=
  by
  rw [← s.neg_le_neg_iff _ hu, neg_zero] at hsu
  rw [← s.neg_le_neg_iff _ hv, neg_zero] at hsv
  have := of_diff_eq_zero_of_symmDiff_eq_zero_positive hu hv hsu hsv
  simp only [Pi.neg_apply, neg_eq_zero, coe_neg] at this
  exact this hs

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