English
If s ∈ S and t ∈ T with S, T families of sets, and S, T are measurable, and the big independence hypothesis holds, then IndepSet s t κ μ.
Русский
Если s принадлежит S, t принадлежит T, при условии измеримости и независимости, то IndepSet s t κ μ.
LaTeX
$$$IndepSets S T κ μ \Rightarrow IndepSet s t κ μ$$$
Lean4
theorem indepSet_of_mem {_m0 : MeasurableSpace Ω} (hs : s ∈ S) (ht : t ∈ T) (hs_meas : MeasurableSet s)
(ht_meas : MeasurableSet t) (κ : Kernel α Ω) (μ : Measure α) [IsZeroOrMarkovKernel κ]
(h_indep : IndepSets S T κ μ) : IndepSet s t κ μ :=
(indepSet_iff_measure_inter_eq_mul hs_meas ht_meas κ μ).mpr (h_indep s t hs ht)