hausdorffMeasure_measurePreserving_funUnique

English

There is a measure-preserving equivalence (funUnique) that preserves the Hausdorff measure for all d.

Русский

Существуют эквивалентности funUnique сохраняющие меру Хаусдорфа для всех d.

LaTeX

$$$\text{hausdorffMeasure}_{d}$ preserves under $\text{funUnique}$$$

Lean4

theorem hausdorffMeasure_measurePreserving_funUnique [Unique ι] [SecondCountableTopology X] (d : ℝ) :
    MeasurePreserving (MeasurableEquiv.funUnique ι X) μH[d] μH[d] :=
  (IsometryEquiv.funUnique ι X).measurePreserving_hausdorffMeasure _

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