indepSets_singleton_iff — Mathlib

English

Two singleton sigma-algebras generated by sets s and t are independent if and only if μ(s ∩ t) = μ(s) μ(t).

Русский

Две сигма-алгебры, порожденные множествами s и t, независимы тогда и только тогда, когда μ(s ∩ t) = μ(s) μ(t).

LaTeX

$$$IndepSets(\\{s\\}, \\{t\\}; \\mu) \\iff \\mu(s \\cap t) = \\mu(s) \\mu(t)$$$

Lean4

theorem indepSets_singleton_iff {s t : Set Ω} : IndepSets { s } { t } μ ↔ μ (s ∩ t) = μ s * μ t := by
  simp only [IndepSets, Kernel.indepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure, Kernel.const_apply]

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