volume_univ — Mathlib

English

For measurable s, the comap of μ along f equals the image measure of f restricted to s, i.e., comap f μ on t equals μ (f''t) for t ⊆ s.

Русский

Для измеримого s соответствующая операция comap по f равна образу меры μ, ограниченной на s.

LaTeX

$$$\text{comap } f μ \, t = μ (f'' t).$$$

Lean4

theorem volume_univ (hu : NullMeasurableSet u) : volume (univ : Set u) = volume u :=
  by
  rw [Subtype.volume_def, comap_apply₀ _ _ _ _ MeasurableSet.univ.nullMeasurableSet]
  · simp only [image_univ, Subtype.range_coe_subtype, setOf_mem_eq]
  · exact Subtype.coe_injective
  · exact fun t => MeasurableSet.nullMeasurableSet_subtype_coe hu

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