of_inter_eq_of_symmDiff_eq_zero_negative

English

If the symmetric difference of u and v is null under the negative portion, then s(w ∩ u) = s(w ∩ v).

Русский

Если симметрическая разность u и v нулевая на части с отрицательным знаком, то меры на пересечениях равны.

LaTeX

$$$$ (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w) (hsu : s ≤[u] 0) (hsv : s ≤[v] 0) (hs : s (u \Delta v) = 0) : s (w \cap u) = s (w \cap v). $$$$

Lean4

theorem of_inter_eq_of_symmDiff_eq_zero_negative (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w)
    (hsu : s ≤[u] 0) (hsv : s ≤[v] 0) (hs : s (u ∆ v) = 0) : s (w ∩ u) = s (w ∩ v) :=
  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_inter_eq_of_symmDiff_eq_zero_positive hu hv hw hsu hsv
  simp only [Pi.neg_apply, neg_inj, neg_eq_zero, coe_neg] at this
  exact this hs

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