English
The family (s_i) is independent if and only if for every finite subset S of I and every family of sets f(i) with f(i) measurable w.r.t. generateFrom {s_i} for i in S, μ(∩_{i∈S} f(i)) = ∏_{i∈S} μ(f(i)).
Русский
Семейство (s_i) независимо тогда и только тогда, когда для каждого конечного подмножества S ⊆ I и для каждого семейства множеств f(i), измеримых относительно σ({s_i}) для i ∈ S, выполняется μ(∩_{i∈S} f(i)) = ∏_{i∈S} μ(f(i)).
LaTeX
$$$\text{IndepSet}(s,\mu) \iff \forall S\in\mathcal{F}, \forall f:\, \iota\to \text{Set} \; (\forall i\in S,\; \text{MeasurableSet}[\ generateFrom{\{s_i\}}](f(i))) \,\Rightarrow\, \mu\left(\bigcap_{i\in S} f(i)\right) = \prod_{i\in S} \mu(f(i))$$$
Lean4
theorem iIndepSet_iff (s : ι → Set Ω) (μ : Measure Ω) :
iIndepSet s μ ↔
∀ (s' : Finset ι) {f : ι → Set Ω} (_H : ∀ i, i ∈ s' → MeasurableSet[generateFrom {s i}] (f i)),
μ (⋂ i ∈ s', f i) = ∏ i ∈ s', μ (f i) :=
by simp only [iIndepSet_iff_iIndep, iIndep_iff]
