iIndep_comap_mem_iff — Mathlib

English

The independence of a family of comapped sigma-algebras defined by membership in sets f_i is equivalent to independence of the family iIndepSet f μ.

Русский

Независимость семейства σ-алгебр, полученных через композицию с принадлежностью к множествам f_i, эквивалентна независимости семейства iIndepSet f μ.

LaTeX

$$$iIndep (\lambda i, MeasurableSpace.comap(\cdot \in f_i)\top) μ \iff iIndepSet f μ$$$

Lean4

theorem iIndep_comap_mem_iff {f : ι → Set Ω} : iIndep (fun i => MeasurableSpace.comap (· ∈ f i) ⊤) μ ↔ iIndepSet f μ :=
  Kernel.iIndep_comap_mem_iff

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