volume_image_subtype_coe — Mathlib

English

If s is measurable and t is a set in s, then the volume of the image of t under the inclusion s → α equals the volume of t (in the subspace s).

Русский

Если s измеримо, а t — подмножество s, то объем изображения t через включение s → α равен объему t в подпространстве s.

LaTeX

$$$ \\mathrm{Vol}_{\\alpha}((\\iota_s)'' t) = \\mathrm{Vol}_{s}(t) $$$

Lean4

theorem volume_image_subtype_coe {s : Set α} (hs : MeasurableSet s) (t : Set s) :
    volume ((↑) '' t : Set α) = volume t :=
  (comap_subtype_coe_apply hs volume t).symm

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