iIndepSets' — Mathlib

English

From independence, derive iIndepSets with all measurable sets.

Русский

Из независимости получить iIndepSets для всех измеримых множеств.

LaTeX

$$$iIndep m μ \Rightarrow iIndepSets (\lambda x. {S | MeasurableSet[S]}) μ$$$

Lean4

theorem iIndepSets' {m : ι → MeasurableSpace Ω} {_ : MeasurableSpace Ω} {μ : Measure Ω} (hμ : iIndep m μ) :
    iIndepSets (fun x ↦ {s | MeasurableSet[m x] s}) μ :=
  (iIndep_iff_iIndepSets _ _).1 hμ

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