iIndep — Mathlib

English

If iIndepFun f μ holds, then the collection of pullback sigma-algebras via f is independent.

Русский

Если выполняется iIndepFun f μ, то множество обратно-потянутых сигма-алгебр через f независимы.

LaTeX

$$$\text{iIndepFun}(f, μ) \Rightarrow \text{iIndep}(\;i \mapsto (m_i).comap(f_i)\; , μ)$$$

Lean4

protected theorem iIndep {m : ∀ i, MeasurableSpace (κ i)} {f : ∀ x : ι, Ω → κ x} (hf : iIndepFun f μ) :
    iIndep (fun x ↦ (m x).comap (f x)) μ :=
  hf

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