hausdorffMeasure_image

Mathlib.MeasureTheory.Measure.Hausdorff

URI: https://scilib.ai/kg/mathlib#IsometryEquiv.hausdorffMeasure_image

← MathLib Explorer

English

For an isometry equivalence e, μH^d(e[S]) = μH^d(S).

Русский

Для эквивалента изометрии: мера образа сохраняется.

LaTeX

$$$\mu_H^{d}(e''S) = \mu_H^{d}(S)$$$

Lean4

@[simp]
theorem hausdorffMeasure_image (e : X ≃ᵢ Y) (d : ℝ) (s : Set X) : μH[d] (e '' s) = μH[d] s :=
  e.isometry.hausdorffMeasure_image (Or.inr e.surjective) s

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru