English
Let ι be a type with a unique element and let X be a family of spaces X i indexed by ι, each carrying a measure space structure. Then the canonical measurable equivalence that collapses the indexed product ∏ i∈ι X i to the single space X i0 (where i0 is the unique index) preserves the volume (product) measure.
Русский
Пусть ι—тип с уникальным элементом и пусть X={X_i} задаёт семейство пространств, каждая из которых несёт структуру пространства меры. Тогда каноническое измеримое эквивалентное отображение, переводящее произведение по индексу ∏ i∈ι X_i в единственное пространство X_{i0} (где i0 — единственный индекс), сохраняет меру объёма (произведение мер).
LaTeX
$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.piUnique}(X)\bigr)\; \mathrm{volume}\; \mathrm{volume} $$$
Lean4
theorem volume_preserving_piUnique (X : ι → Type*) [Unique ι] [∀ i, MeasureSpace (X i)] :
MeasurePreserving (MeasurableEquiv.piUnique X) volume volume :=
measurePreserving_piUnique _
