English
If μ is s-finite, then for every measurable set s and any set t, μ(toMeasurable μ t ∩ s) = μ(t ∩ s).
Русский
Если μ является s‑конечной мерой, то для любого измеримого множества s и любого множества t выполняется μ(toMeasurable μ t ∩ s) = μ(t ∩ s).
LaTeX
$$$[SFinite μ] \rightarrow (hs : MeasurableSet s) \rightarrow \forall t, μ (toMeasurable μ t \cap s) = μ (t \cap s)$$$
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) = μ (t ∩ s)`.
This only holds when `μ` is s-finite -- for example for σ-finite measures. For a version without
this assumption (but requiring that `t` has finite measure), see `measure_toMeasurable_inter`. -/
theorem measure_toMeasurable_inter_of_sFinite [SFinite μ] {s : Set α} (hs : MeasurableSet s) (t : Set α) :
μ (toMeasurable μ t ∩ s) = μ (t ∩ s) :=
measure_toMeasurable_inter_of_sum hs (fun _ ↦ measure_ne_top _ t) (sum_sfiniteSeq μ).symm
