IndepSets_iff — Mathlib

English

Two equivalent formulations of independence for collections of sets are equivalent to the usual product-rule formulation.

Русский

Две эквивалентные формулировки независимости для коллекций множеств эквивалентны обычной формулировке через произведение мер.

LaTeX

$$$IndepSets s1 s2 μ \iff ∀ t1 ∈ s1, t2 ∈ s2, μ(t1 ∩ t2) = μ(t1) μ(t2)$$$

Lean4

theorem IndepSets_iff (s1 s2 : Set (Set Ω)) (μ : Measure Ω) :
    IndepSets s1 s2 μ ↔ ∀ t1 t2 : Set Ω, t1 ∈ s1 → t2 ∈ s2 → (μ (t1 ∩ t2) = μ t1 * μ t2) := by
  simp only [IndepSets, Kernel.IndepSets, ae_dirac_eq, Filter.eventually_pure, Kernel.const_apply]

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