coe_toMeasurableEquiv

Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

URI: https://scilib.ai/kg/mathlib#LinearIsometryEquiv.coe_toMeasurableEquiv

English

The Haar measure defined by any basis equals the volume measure.

Русский

Мера Хаара, заданная по любому базису, равна объёмной мере.

LaTeX

$$$\\text{HBasis}_{\\text{basis}} = \\text{volume measure}$ for any orthonormal basis.$$

Lean4

@[simp]
theorem coe_toMeasurableEquiv : (f.toMeasurableEquiv : E → F) = f :=
  rfl

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

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

Разделы

Аффилиация

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