hausdorffMeasure_preimage — Mathlib

English

For isometries, the preimage satisfies μH^d(f^{-1}(s)) = μH^d(s ∩ range f).

Русский

Для изометрий: предобраз удовлетворяет μ_H^d(f^{-1}(s)) = μ_H^d(s ∩ range f).

LaTeX

$$$μ_H^{d}(f^{-1}(s)) = μ_H^{d}(s \cap \mathrm{range}(f))$$$

Lean4

theorem hausdorffMeasure_preimage (hf : Isometry f) (hd : 0 ≤ d ∨ Surjective f) (s : Set Y) :
    μH[d] (f ⁻¹' s) = μH[d] (s ∩ range f) := by rw [← hf.hausdorffMeasure_image hd, image_preimage_eq_inter_range]

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