iIndepSet_iff_iIndepSets_singleton

English

For a family of sets f_i, independence of the family in the iIndepSet sense is equivalent to independence of the corresponding singleton families {f_i} in the iIndepSets sense.

Русский

Для семейства множеств f_i независимость в смысле iIndepSet эквивалентна независимости соответствующих семейств-синонимов {f_i} в смысле iIndepSets.

LaTeX

$$$iIndepSet f κ μ \;\Longleftrightarrow\; iIndepSets (i\mapsto {f_i}) κ μ$$

Lean4

theorem iIndepSet_iff_iIndepSets_singleton {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} {f : ι → Set Ω}
    (hf : ∀ i, MeasurableSet (f i)) : iIndepSet f κ μ ↔ iIndepSets (fun i ↦ {f i}) κ μ :=
  ⟨iIndep.iIndepSets fun _ ↦ rfl,
    iIndepSets.iIndep _ (fun i ↦ generateFrom_le <| by rintro t (rfl : t = _); exact hf _) _
      (fun _ ↦ IsPiSystem.singleton _) fun _ ↦ rfl⟩

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