iIndepSet_iff_iIndep — Mathlib

English

Let (Ω, μ) be a probability space and (s_i) a family of events indexed by i in I. The events s_i are independent if and only if the sigma-algebras they generate are independent.

Русский

Пусть (Ω, μ) — вероятность пространство, а {s_i} — семейство событий, индексируемое i ∈ I. События s_i независимы тогда и только тогда, когда соответствующие им сигма-алгебры σ({s_i}) независимы.

LaTeX

$$$\text{IndepSet}(s,\mu) \iff \text{Indep}\bigl(i \mapsto \ generateFrom\{s(i)\}\bigr)\,\mu$$$

Lean4

theorem iIndepSet_iff_iIndep (s : ι → Set Ω) (μ : Measure Ω) : iIndepSet s μ ↔ iIndep (fun i ↦ generateFrom {s i}) μ :=
  by simp only [iIndepSet, iIndep, Kernel.iIndepSet]

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