English
If a set t matches a set u in measure on almost every point (ae), then μ(t ∩ s) = μ(u ∩ s) for any s with measurable intersection.
Русский
Если сae тождественны на почти всю точку по мере μ, тогда μ(t ∩ s) = μ(u ∩ s) для любого измеримого s.
LaTeX
$$$$ \mu\bigl(t \cap s\bigr) = \mu\bigl(u \cap s\bigr) \quad\text{whenever } \mu t = \mu u \text{ and } t \subseteq u.$$$$
Lean4
/-- If `u` is a superset of `t` with the same (finite) measure (both sets possibly non-measurable),
then for any measurable set `s` one also has `μ (t ∩ s) = μ (u ∩ s)`. -/
theorem measure_inter_eq_of_measure_eq {s t u : Set α} (hs : MeasurableSet s) (h : μ t = μ u) (htu : t ⊆ u)
(ht_ne_top : μ t ≠ ∞) : μ (t ∩ s) = μ (u ∩ s) :=
by
rw [h] at ht_ne_top
refine le_antisymm (by gcongr) ?_
have A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s) :=
calc
μ (u ∩ s) + μ (u \ s) = μ u := measure_inter_add_diff _ hs
_ = μ t := h.symm
_ = μ (t ∩ s) + μ (t \ s) := (measure_inter_add_diff _ hs).symm
_ ≤ μ (t ∩ s) + μ (u \ s) := by gcongr
have B : μ (u \ s) ≠ ∞ := (lt_of_le_of_lt (measure_mono diff_subset) ht_ne_top.lt_top).ne
exact ENNReal.le_of_add_le_add_right B A
