English
Two sigma-algebras m1 and m2 are independent with respect to κ μ if and only if for every measurable sets s, t in m1, m2 respectively, IndepSet s t κ μ holds.
Русский
Две сигма-алгебры m1 и m2 независимы относительно κ μ тогда и только тогда, когда для любых измеримых множеств s∈m1 и t∈m2 выполняется IndepSet s t κ μ.
LaTeX
$$$Indep m_1 m_2 κ μ \Leftrightarrow \forall s,t, MeasurableSet[m_1] s → MeasurableSet[m_2] t → IndepSet s t κ μ$$$
Lean4
theorem indep_iff_forall_indepSet (m₁ m₂ : MeasurableSpace Ω) {_m0 : MeasurableSpace Ω} (κ : Kernel α Ω)
(μ : Measure α) : Indep m₁ m₂ κ μ ↔ ∀ s t, MeasurableSet[m₁] s → MeasurableSet[m₂] t → IndepSet s t κ μ :=
⟨fun h => fun _s _t hs ht => h.indepSet_of_measurableSet hs ht, fun h s t hs ht =>
h s t hs ht s t (measurableSet_generateFrom (Set.mem_singleton s))
(measurableSet_generateFrom (Set.mem_singleton t))⟩
