meas_iInter — Mathlib

English

With finite index, iIndep yields the usual multi-set intersection product formula.

Русский

При конечном индексе iIndep даёт обычную формулу для пересечения множеств и произведения мер.

LaTeX

$$$[Fintype ι] \ (hμ : iIndep m μ) (hs : ∀ i, MeasurableSet[m i] (s i)) : μ (⋂ i, s i) = ∏ i, μ (s i)$$$

Lean4

theorem meas_iInter [Fintype ι] (hμ : iIndep m μ) (hs : ∀ i, MeasurableSet[m i] (s i)) : μ (⋂ i, s i) = ∏ i, μ (s i) :=
  by simp [← hμ.meas_biInter fun _ _ ↦ hs _]

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