condIndepSet_empty_left — Mathlib

English

Let Ω be a standard Borel space with finite measure μ, and let m' be a sub-σ-algebra of Ω with m' ≤ mΩ. Then for any subset s of Ω, the conditional independence of the empty family from s holds: CondIndepSet m' hm' ∅ s μ.

Русский

Пусть Ω — стандартное пространство Бореля, μ — конечная мера, m' — подсистема σ-алгей Ω с m' ≤ mΩ. Тогда для любой подмножества s выполняется условная независимость пустого множества от σ-алгей, порождаемой s: CondIndepSet m' hm' ∅ s μ.

LaTeX

$$$\mathrm{CondIndepSet}(m', hm', \emptyset, s, \mu)$$$

Lean4

theorem condIndepSet_empty_left (s : Set Ω) : CondIndepSet m' hm' ∅ s μ :=
  Kernel.indepSet_empty_left s

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