English
For an independent family iIndepFun f μ, the measure of a finite intersection equals the finite product of measures, given appropriate measurability of the components.
Русский
Для независимого семейства iIndepFun f μ, мера пересечения конечного набора равно произведению мер компонентов, при подходящей измеримости.
LaTeX
$$$\text{IndepFun}(f, μ) \to \; (\forall S, (\forall i \in S, MeasurableSet[(m_i).comap(f_i)](s_i)) \Rightarrow μ(\bigcap_{i\in S} s_i) = \prod_{i\in S} μ(s_i))$$$
Lean4
theorem iIndepFun_iff {β : ι → Type*} (m : ∀ x : ι, MeasurableSpace (β x)) (f : ∀ x : ι, Ω → β x) (μ : Measure Ω) :
iIndepFun f μ ↔
∀ (s : Finset ι) {f' : ι → Set Ω} (_H : ∀ i, i ∈ s → MeasurableSet[(m i).comap (f i)] (f' i)),
μ (⋂ i ∈ s, f' i) = ∏ i ∈ s, μ (f' i) :=
by simp only [iIndepFun_iff_iIndep, iIndep_iff]
