iIndepSets_singleton_iff — Mathlib

English

Independence of singleton-indexed sets is equivalent to a finite intersection/product equality over all finite index sets.

Русский

Независимость множества с одиночной интенцификацией индексов эквивалентна равенству произведения и пересечения по всем конечным множествам индексов.

LaTeX

$$$iIndepSets(\lambda i, {s_i}) μ \iff ∀ t, μ(⋂ i∈t s_i) = ∏ i∈t μ(s_i)$$$

Lean4

theorem iIndepSets_singleton_iff {s : ι → Set Ω} :
    iIndepSets (fun i ↦ {s i}) μ ↔ ∀ t, μ (⋂ i ∈ t, s i) = ∏ i ∈ t, μ (s i) := by
  simp_rw [iIndepSets, Kernel.iIndepSets_singleton_iff, ae_dirac_eq, Filter.eventually_pure, Kernel.const_apply]

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