meas_biInter — Mathlib

English

For iIndepSets, the intersection-measure equality reduces to a product over indices for finite index sets.

Русский

Для iIndepSets пересечение множеств имеет меру равную произведению мер по индексам для конечных наборов индексов.

LaTeX

$$$(iIndepSets π μ) ⇔ ∀ (s : Finset ι) {f : ι → Set Ω}, (∀ i ∈ s, f i ∈ π i) → μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)$$$

Lean4

theorem meas_biInter (hμ : iIndep m μ) (hs : ∀ i, i ∈ S → MeasurableSet[m i] (s i)) :
    μ (⋂ i ∈ S, s i) = ∏ i ∈ S, μ (s i) :=
  (iIndep_iff _ _).1 hμ _ hs

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