Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
inst✝ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : iIndep m
i j : ι
hij : i ≠ j
⊢ IndepSets ((fun x => MeasurableSet) i) ((fun x => MeasurableSet) j)
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
inst✝ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : iIndep m
i j : ι
hij : i ≠ j
⊢ Indep (m i) (m j)
change IndepSets ((fun x => MeasurableSet[m x]) i) ((fun x => MeasurableSet[m x]) j) μ
no goals
Ω : Type u_1
ι : Type u_2
m : ι → MeasurableSpace Ω
inst✝ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
h_indep : iIndep m
i j : ι
hij : i ≠ j
⊢ IndepSets ((fun x => MeasurableSet) i) ((fun x => MeasurableSet) j)
exact iIndepSets.indepSets h_indep hij