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)