indep — Mathlib

English

Reiterates the singleton iIndepSets criterion in a variant form.

Русский

Повторяет критерий iIndepSets singleton в другой форме.

LaTeX

$$iIndepSets_singleton_iff {s : ι → Set Ω} κ μ ↔ ∀ S : Finset ι, ∀ᵐ a ∂μ, κ a (⋂ i ∈ S, s i) = ∏ i ∈ S κ a (s i)$$

Lean4

theorem indep {m : ι → MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
    (h_indep : iIndep m κ μ) {i j : ι} (hij : i ≠ j) : Indep (m i) (m j) κ μ :=
  iIndepSets.indepSets h_indep hij

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