Indep_iff_IndepSets — Mathlib

English

Independence of two measurable spaces is equivalent to independence of the corresponding sets of measurable sets.

Русский

Независимость двух измеримых пространств эквивалентна независимости соответствующих множеств измеримых множеств.

LaTeX

$$$Indep m1 m2 μ \iff IndepSets {s | MeasurableSet[m1] s} {s | MeasurableSet[m2] s} μ$$

Lean4

theorem Indep_iff_IndepSets (m₁ m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : Measure Ω) :
    Indep m₁ m₂ μ ↔ IndepSets {s | MeasurableSet[m₁] s} {s | MeasurableSet[m₂] s} μ := by
  simp only [Indep, IndepSets, Kernel.Indep]

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