meas_biInter — Mathlib

English

If h : iIndep π κ μ, then for any finite S and sets f i ∈ π i, the intersection of the f i has measure equal to the product of the individual measures almost surely.

Русский

Если h : iIndep π κ μ, то для любого конечного множества S и множеств f i ∈ π i пересечение f i имеет меру, равную произведению отдельных мер почти surely.

LaTeX

$$$ (h : iIndep π κ μ) \\Rightarrow (s : Finset ι) \\to (f : ι \\to Set Ω) \\to (\\forall i, i ∈ s → f i ∈ π i) \\Rightarrow \\forall a, κ a (\\bigcap_{i ∈ s} f i) = \\prod_{i ∈ s} κ a (f i) $$$

Lean4

theorem meas_biInter (hμ : iIndep m κ μ) (hs : ∀ i, i ∈ S → MeasurableSet[m i] (s i)) :
    ∀ᵐ a ∂μ, κ a (⋂ i ∈ S, s i) = ∏ i ∈ S, κ a (s i) :=
  hμ _ hs

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