IndepSet_iff_Indep — Mathlib

English

Two events s and t are independent if and only if the sigma-algebras generated by {s} and {t} are independent.

Русский

Два события s и t независимы тогда и только тогда, когда сигма-алгебры, порождённые {s} и {t}, независимы.

LaTeX

$$$\text{IndepSet}(s,t,\mu) \iff \text{Indep}(\sigma(\{s\}), \sigma(\{t\} ), \mu)$$$

Lean4

theorem IndepSet_iff_Indep (s t : Set Ω) (μ : Measure Ω) :
    IndepSet s t μ ↔ Indep (generateFrom { s }) (generateFrom { t }) μ := by
  simp only [IndepSet, Indep, Kernel.IndepSet]

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