English
If π is a family of σ-algebras and κ is a kernel such that iIndepSets π κ μ holds, then for any finite collection s ⊂ ι and any family f with f(i) ∈ π_i for i ∈ s, almost everywhere with respect to μ we have κ a(⋂_{i∈s} f(i)) = ∏_{i∈s} κ a(f(i)).
Русский
Если π — семейство σ-алгебр и κ — ядро так, что выполняется iIndepSets π κ μ, то для любой конечной подмножества s ⊂ ι и любой семейства f, где f(i) ∈ π_i для i∈s, почти все a удовлетворяют: κ a(⋂_{i∈s} f(i)) = ∏_{i∈s} κ a(f(i)).
LaTeX
$$$ (h \\!:\\! iIndepSets \\ π \\ κ \\ μ) \\Rightarrow (s : Finset\\ ι) \\to (f : ι \\to Set\\ Ω) \\to (\\forall i \\in s, f(i) \\in π_i) \\Rightarrow \\forall a, κ a (\\bigcap_{i\\in s} f(i)) = \\prod_{i\\in s} κ a (f(i)) \\; (\\aqeμ).$$$
Lean4
theorem meas_biInter (h : iIndepSets π κ μ) (s : Finset ι) {f : ι → Set Ω} (hf : ∀ i, i ∈ s → f i ∈ π i) :
∀ᵐ a ∂μ, κ a (⋂ i ∈ s, f i) = ∏ i ∈ s, κ a (f i) :=
h s hf
