meas_biInter — Mathlib

English

Given an iIndepSet f κ μ, and a finite set s, the measure of the intersection of all f_i over i in s equals the product of the measures of each f_i, almost surely with respect to μ.

Русский

Для iIndepSet f κ μ и конечного множества s мера пересечения всех f_i по i∈s равна произведению мер каждого f_i, почти surely по μ.

LaTeX

$$$\forall s, \mathrm{ae}_{μ} \; κ a\left(\bigcap_{i\in s} f_i\right)=\prod_{i\in s} κ a(f_i)$$$

Lean4

theorem meas_biInter {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} {f : ι → Set Ω} (h : iIndepSet f κ μ)
    (s : Finset ι) : ∀ᵐ a ∂μ, κ a (⋂ i ∈ s, f i) = ∏ i ∈ s, κ a (f i) :=
  iIndep.iIndepSets (fun _ ↦ rfl) h _ (by simp)

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