measurePreserving_funUnique — Mathlib

English

Let β be a space with a measure μ, and let α be a type with a unique element. The canonical map funUnique α β from α → β to β is measure-preserving between the product measure on α-indexed copies of μ and μ itself.

Русский

Пусть β - пространство с мерой μ, а α — тип с единственным элементом. Каноническое отображение funUnique α β из α → β в β сохраняет меру: произведение μ по α сохраняет меру μ.

LaTeX

$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.funUnique}(\alpha,\beta)\bigr)\; (\mathrm{Measure.pi}\;\lambda\,i.\mu)\; \mu $$$

Lean4

theorem measurePreserving_funUnique {β : Type u} {_m : MeasurableSpace β} (μ : Measure β) (α : Type v) [Unique α] :
    MeasurePreserving (MeasurableEquiv.funUnique α β) (Measure.pi fun _ : α => μ) μ :=
  measurePreserving_piUnique _

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