volume_pi

Mathlib.MeasureTheory.Constructions.Pi

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

English

The volume measure on the product space ∏ α_i equals the product of the volume measures on each α_i.

Русский

Объемная мера на произведении пространств равна произведению объемов на каждом пространстве.

LaTeX

$$$volume = \pi(volume)$$$

Lean4

theorem volume_pi [∀ i, MeasureSpace (α i)] : (volume : Measure (∀ i, α i)) = Measure.pi fun _ => volume :=
  rfl

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

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

Разделы

Аффилиация

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