map_coe_volume — Mathlib

English

Let s be a measurable subset of α. The pushforward of the volume measure on s along the inclusion map i: s → α equals the volume measure restricted to s.

Русский

Пусть s — измеримое подмножество α. Перенос объема по включению i: s → α равен ограниченному объему на s.

LaTeX

$$$ (i_s)_*\, \\mathrm{Vol}_s = \\mathrm{Vol}_\\alpha|_s, \\quad i_s: s \\hookrightarrow \\alpha $$$

Lean4

theorem map_coe_volume {s : Set α} (hs : MeasurableSet s) : volume.map ((↑) : s → α) = restrict volume s := by
  rw [volume_set_coe_def, (MeasurableEmbedding.subtype_coe hs).map_comap volume, Subtype.range_coe]

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