hausdorffMeasure_measurePreserving_piFinTwo

English

For a two-way product of finite types, the Hausdorff measure is preserved under the piFinTwo equivalence, i.e., π-finite two-ary product preserves μH[d].

Русский

Для произведения двух конечных типов μH[d] сохраняется под эквивалентностью piFinTwo.

LaTeX

$$$\text{hausdorffMeasure } d$ is preserved by $\text{piFinTwo}$$$

Lean4

theorem hausdorffMeasure_measurePreserving_piFinTwo (α : Fin 2 → Type*) [∀ i, MeasurableSpace (α i)]
    [∀ i, EMetricSpace (α i)] [∀ i, BorelSpace (α i)] [∀ i, SecondCountableTopology (α i)] (d : ℝ) :
    MeasurePreserving (MeasurableEquiv.piFinTwo α) μH[d] μH[d] :=
  (IsometryEquiv.piFinTwo α).measurePreserving_hausdorffMeasure _

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