English
If s and t are null-measurable sets with μ(s) = μ(t) and μ(s ∩ t) < ∞, then μ(s \ t) = μ(t \ s).
Русский
Пусть s и t — нулево измеримые множества, μ(s) = μ(t) и μ(s ∩ t) < ∞; тогда μ(s \ t) = μ(t \ s).
LaTeX
$$$\mu(s \ t) = \mu(t \ s)$ при условии: $\text{NullMeasurableSet } s \mu$, $\text{NullMeasurableSet } t \mu$, $\mu s = \mu t$, $\mu(s \cap t) \neq \infty$$$
Lean4
/-- If `s` and `t` are null measurable sets of equal measure
and their intersection has finite measure,
then `s \ t` and `t \ s` have equal measures too. -/
theorem measure_diff_symm (hs : NullMeasurableSet s μ) (ht : NullMeasurableSet t μ) (h : μ s = μ t)
(hfin : μ (s ∩ t) ≠ ∞) : μ (s \ t) = μ (t \ s) := by
rw [← ENNReal.add_right_inj hfin, measure_inter_add_diff₀ _ ht, inter_comm, measure_inter_add_diff₀ _ hs, h]
