English
Let s be a (null) measurable set and t a measurable set in α. Then the volume of the preimage of t under the inclusion s → α equals the volume of t ∩ s.
Русский
Пусть s — нулево измеримое множество и t — измеримое множество в α. Тогда объем прообраза t по включению s → α равен объему t ∩ s.
LaTeX
$$$ \\mathrm{Vol}(((\\uparrow) : s \\to \\alpha)^{-1} t) = \\mathrm{Vol}(t \\cap s) $$$
Lean4
@[simp]
theorem volume_preimage_coe (hs : NullMeasurableSet s) (ht : MeasurableSet t) :
volume (((↑) : s → α) ⁻¹' t) = volume (t ∩ s) := by
rw [volume_set_coe_def,
comap_apply₀ _ _ Subtype.coe_injective (fun h => MeasurableSet.nullMeasurableSet_subtype_coe hs)
(measurable_subtype_coe ht).nullMeasurableSet,
image_preimage_eq_inter_range, Subtype.range_coe]
