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⟩