iIndep_comap_mem_iff — Mathlib

English

The iIndep of a family of comaps is equivalent to the iIndepSet property of the index family.

Русский

Независимость по множеству сопряжений эквивалентна свойству iIndepSet для множества индексов.

LaTeX

$$iIndep (λ i, comap (· ∈ f i) ⊤) κ μ ↔ iIndepSet f κ μ$$

Lean4

theorem iIndep_comap_mem_iff {f : ι → Set Ω} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} :
    iIndep (fun i => MeasurableSpace.comap (· ∈ f i) ⊤) κ μ ↔ iIndepSet f κ μ := by
  simp_rw [← generateFrom_singleton, iIndepSet]

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