volume_set_coe_def — Mathlib

English

For a measure space and a subtype, the volume on the set of the subtype equals the comap of the ambient volume on the subtype set.

Русский

Объем множества в подтипе равен комап-объему окружающей меры на множество из подтипа.

LaTeX

$$$\text{volume}_{u}(\mathrm{Set.univ}) = \mathrm{comap}((\uparrow) : u \to \alpha)\; \mathrm{volume}$$$

Lean4

theorem volume_set_coe_def (s : Set α) : (volume : Measure s) = comap ((↑) : s → α) volume :=
  rfl

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