English
For any null-measurable u, the volume of the unit interval of the subtype equals the volume of the subtype, i.e., the total measure of the subtype matches the ambient volume.
Русский
Для любого нулемеряемого u мерой является равенство: объём универсума подтипа равен объему самого подтипа.
LaTeX
$$$\text{volume}(\mathrm{univ}_{u}) = \mathrm{volume}(u).$$$
Lean4
/-- In a measure space, one can restrict the measure to a subtype to get a new measure space.
Not registered as an instance, as there are other natural choices such as the normalized restriction
for a probability measure, or the subspace measure when restricting to a vector subspace. Enable
locally if needed with `attribute [local instance] Measure.Subtype.measureSpace`. -/
noncomputable def measureSpace : MeasureSpace (Subtype p) where volume := Measure.comap Subtype.val volume
