pi_empty_univ — Mathlib

English

If ι is finite and the index set is empty, the product measure of the empty family equals the unit measure on the empty product space.

Русский

Если индексный набор пуст, то произведение мер по пустому индексу равно единичной мере на пустом произведении пространств.

LaTeX

$$$(\pi\mu)(\mathrm{univ}) = 1$$$

Lean4

@[simp]
theorem pi_empty_univ {α : Type*} [Fintype α] [IsEmpty α] {β : α → Type*} {m : ∀ α, MeasurableSpace (β α)}
    (μ : ∀ a : α, Measure (β a)) : Measure.pi μ (Set.univ) = 1 := by rw [pi_of_empty, measure_univ]

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