indepSet_of_measurableSet — Mathlib

English

If independence holds between σ-algebras m1 and m2 with respect to μ, and s and t are measurable in m1 and m2 respectively, then s and t are independent sets under μ.

Русский

Если существование независимости между σ-алгебрами m1 и m2 относительно μ, и множества s и t измеримы относительно соответственно m1 и m2, то s и t независимы по μ.

LaTeX

$$$Indep(m_1,m_2,μ) \implies (s\in m_1, t\in m_2) \Rightarrow IndepSet(s,t,μ)$$$

Lean4

theorem indepSet_of_measurableSet (h_indep : Indep m₁ m₂ μ) {s t : Set Ω} (hs : MeasurableSet[m₁] s)
    (ht : MeasurableSet[m₂] t) : IndepSet s t μ :=
  Kernel.Indep.indepSet_of_measurableSet h_indep hs ht

Похожие утверждения