indepSet_iff_indepSets_singleton — Mathlib

English

For measurable sets s and t, independence of s and t is equivalent to independence of the singleton families {s} and {t}.

Русский

Для измеримых множеств s и t независимость s и t эквивалентна независимости пар одиночных множеств {s} и {t}.

LaTeX

$$$IndepSet\,s\,t\ κ\ μ \Leftrightarrow IndepSets\{s\}\{t\}\ κ\ μ$$

Lean4

theorem indepSet_iff_indepSets_singleton {m0 : MeasurableSpace Ω} (hs_meas : MeasurableSet s)
    (ht_meas : MeasurableSet t) (κ : Kernel α Ω) (μ : Measure α) [IsZeroOrMarkovKernel κ] :
    IndepSet s t κ μ ↔ IndepSets { s } { t } κ μ :=
  ⟨Indep.indepSets, fun h =>
    IndepSets.indep (generateFrom_le fun u hu => by rwa [Set.mem_singleton_iff.mp hu])
      (generateFrom_le fun u hu => by rwa [Set.mem_singleton_iff.mp hu]) (IsPiSystem.singleton s)
      (IsPiSystem.singleton t) rfl rfl h⟩

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