isAddHaarMeasure_volume_pi

Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

URI: https://scilib.ai/kg/mathlib#MeasureTheory.isAddHaarMeasure_volume_pi

English

The volume measure on the π-indexed space is an additive Haar measure.

Русский

Объемная мера на пространстве с индексом π является мерой Хаара по суммируемости.

LaTeX

$$$\text{IsAddHaarMeasure } (\text{volume} : \text{Measure}((\iota \to \mathbb{R})))$$$

Lean4

theorem isAddHaarMeasure_volume_pi (ι : Type*) [Fintype ι] : IsAddHaarMeasure (volume : Measure (ι → ℝ)) :=
  inferInstance

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

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

Разделы

Аффилиация

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