iIndepSet_iff_meas_biInter — Mathlib

English

An iIndepSet is equivalent to a condition that for every finite index set S, and for every finite collection of sets, the joint measure equals the product of their marginal measures almost everywhere.

Русский

iIndepSet эквивалентно условию: для каждого конечного множества индексов S и для любой конечной коллекции множеств, совместная мера равна произведению маргинальных мер почти наверху.

LaTeX

$$$iIndepSet f κ μ \Leftrightarrow \forall S, \forall_{sets} ...$$

Lean4

theorem iIndepSet_iff_meas_biInter {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} {f : ι → Set Ω}
    (hf : ∀ i, MeasurableSet (f i)) : iIndepSet f κ μ ↔ ∀ s, ∀ᵐ a ∂μ, κ a (⋂ i ∈ s, f i) = ∏ i ∈ s, κ a (f i) :=
  (iIndepSet_iff_iIndepSets_singleton hf).trans iIndepSets_singleton_iff

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