condIndepSet_iff_condIndepSets_singleton

English

Equivalence condIndepSet_condIndepSets_singleton: CondIndepSet m' hm' s μ ↔ CondIndepSets m' hm' {s} μ.

Русский

Эквивалентность CondIndepSet и CondIndepSets с сигма-алгебрами, порождёнными одиночными множествами: {s}.

LaTeX

$$$CondIndepSet(m', hm', s, μ) \\iff CondIndepSets(m', hm', {s}, μ)$$$

Lean4

theorem condIndepSet_iff_condIndepSets_singleton {s t : Set Ω} (hs_meas : MeasurableSet s) (ht_meas : MeasurableSet t)
    (μ : Measure Ω) [IsFiniteMeasure μ] : CondIndepSet m' hm' s t μ ↔ CondIndepSets m' hm' { s } { t } μ :=
  Kernel.indepSet_iff_indepSets_singleton hs_meas ht_meas _ _

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