volume_subtype_coe_le_volume — Mathlib

English

If volume of t is 0, then the image of t under the subtype inclusion also has volume 0.

Русский

Если объем t равен 0, то образ t через включение подтипа имеет объем 0.

LaTeX

$$$\text{volume}(t) = 0 \Rightarrow \text{volume}(((↑) : u → \delta) '' t) = 0.$$$

Lean4

theorem volume_subtype_coe_le_volume (hu : NullMeasurableSet u) (t : Set u) : volume (((↑) : u → δ) '' t) ≤ volume t :=
  measure_subtype_coe_le_comap hu t

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