measurePreserving_coe — Mathlib

English

The inclusion map I → ℝ is measure-preserving from volume on I to the restricted volume on ℝ.

Русский

Вложение I → ℝ сохраняет меру: объём на I соответствует ограниченному объёму на ℝ.

LaTeX

$$$\text{MeasurePreserving}(\operatorname{Subtype.val}): (\text{volume on } I) \to (\text{volume restricted to } I)$$$

Lean4

theorem measurePreserving_coe : MeasurePreserving ((↑) : I → ℝ) volume (volume.restrict I) :=
  measurePreserving_subtype_coe measurableSet_Icc

Похожие утверждения