English
If t is measurable and μ(t) is finite, then μ(toMeasurable μ t ∩ s) = μ(t ∩ s) for any measurable s.
Русский
Если t измеримо и μ(t) конечна, то μ(toMeasurable μ t ∩ s) = μ(t ∩ s) для любого измеримого s.
LaTeX
$$$$ μ(toMeasurable\, μ\, t \cap s) = μ(t \cap s), \quad (t \text{ measurable}, μ t \neq ∞). $$$$
Lean4
/-- The measurable superset `toMeasurable μ t` of `t` (which has the same measure as `t`)
satisfies, for any measurable set `s`, the equality `μ (toMeasurable μ t ∩ s) = μ (u ∩ s)`.
Here, we require that the measure of `t` is finite. The conclusion holds without this assumption
when the measure is s-finite (for example when it is σ-finite),
see `measure_toMeasurable_inter_of_sFinite`. -/
theorem measure_toMeasurable_inter {s t : Set α} (hs : MeasurableSet s) (ht : μ t ≠ ∞) :
μ (toMeasurable μ t ∩ s) = μ (t ∩ s) :=
(measure_inter_eq_of_measure_eq hs (measure_toMeasurable t).symm (subset_toMeasurable μ t) ht).symm
