measurePreserving_pi_empty — Mathlib

English

If the index set ι is empty, the mapping from the pi-space to the dirac measure on Unit is measure-preserving.

Русский

Если множество индексов пусто, отображение из пространства Pi в единичную меру сохраняет меру.

LaTeX

$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.ofUniqueOfUnique}(\forall i, \alpha i, Unit)\bigr)\; (\mathrm{Measure.pi}\, μ)\; \mathrm{dirac}() $$$

Lean4

theorem measurePreserving_pi_empty {ι : Type u} {α : ι → Type v} [Fintype ι] [IsEmpty ι]
    {m : ∀ i, MeasurableSpace (α i)} (μ : ∀ i, Measure (α i)) :
    MeasurePreserving (MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit) (Measure.pi μ) (Measure.dirac ()) :=
  by
  set e := MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit
  refine ⟨e.measurable, ?_⟩
  rw [Measure.pi_of_empty, Measure.map_dirac e.measurable]

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