Indep_iff — Mathlib

English

A direct equivalence between independence of spaces and independence of their measurable sets holds.

Русский

Простая эквивалентность независимости пространств и независимости измеримых множеств получаемая.

LaTeX

$$$Indep_iff_IndepSets (m1, m2, μ) \iff IndepSets {s | MeasurableSet[m1] s} {s | MeasurableSet[m2] s} μ$$

Lean4

theorem Indep_iff (m₁ m₂ : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω} (μ : Measure Ω) :
    Indep m₁ m₂ μ ↔ ∀ t1 t2, MeasurableSet[m₁] t1 → MeasurableSet[m₂] t2 → μ (t1 ∩ t2) = μ t1 * μ t2 := by
  rw [Indep_iff_IndepSets, IndepSets_iff]; rfl

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