English
For a family of sets f_i, independence of the family in the iIndepSet sense is equivalent to independence of the corresponding singleton families {f_i} in the iIndepSets sense.
Русский
Для семейства множеств f_i независимость в смысле iIndepSet эквивалентна независимости соответствующих семейств-синонимов {f_i} в смысле iIndepSets.
LaTeX
$$$iIndepSet f κ μ \;\Longleftrightarrow\; iIndepSets (i\mapsto {f_i}) κ μ$$
Lean4
theorem iIndepSet_iff_iIndepSets_singleton {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} {f : ι → Set Ω}
(hf : ∀ i, MeasurableSet (f i)) : iIndepSet f κ μ ↔ iIndepSets (fun i ↦ {f i}) κ μ :=
⟨iIndep.iIndepSets fun _ ↦ rfl,
iIndepSets.iIndep _ (fun i ↦ generateFrom_le <| by rintro t (rfl : t = _); exact hf _) _
(fun _ ↦ IsPiSystem.singleton _) fun _ ↦ rfl⟩