indep_iff_forall_indepSet — Mathlib

English

Independence of m1 and m2 with respect to μ is equivalent to independence of all pairs of measurable sets s,t with s in m1 and t in m2.

Русский

Независимость σ-алгебр m1 и m2 по μ эквивалентна независимости всех пар измеримых множеств s,t, где s ∈ m1, t ∈ m2.

LaTeX

$$$Indep(m_1,m_2,μ) \iff ∀ s,t, MeasurableSet[s] \to MeasurableSet[t] \to IndepSet(s,t,μ)$$$

Lean4

theorem indep_iff_forall_indepSet (μ : Measure Ω) :
    Indep m₁ m₂ μ ↔ ∀ s t, MeasurableSet[m₁] s → MeasurableSet[m₂] t → IndepSet s t μ :=
  Kernel.indep_iff_forall_indepSet m₁ m₂ _ _

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