iIndepSets_singleton_iff — Mathlib

English

The iIndepSets condition with singleton slices reduces to a finite-set product equality for every Finset S.

Русский

Условие iIndepSets со срезами-одиночками сводится к равенству произведения для каждого конечного множества S.

LaTeX

$$iIndepSets (f_i) κ μ ↔ ∀ S : Finset ι, ∀ᵐ a ∂μ, κ a (⋂ i ∈ S, s_i) = ∏ i ∈ S κ a (s_i)$$

Lean4

theorem iIndepSets_singleton_iff {s : ι → Set Ω} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} :
    iIndepSets (fun i ↦ {s i}) κ μ ↔ ∀ S : Finset ι, ∀ᵐ a ∂μ, κ a (⋂ i ∈ S, s i) = ∏ i ∈ S, κ a (s i) :=
  by
  refine ⟨fun h S ↦ h S (fun i _ ↦ rfl), fun h S f hf ↦ ?_⟩
  filter_upwards [h S] with a ha
  have : ∀ i ∈ S, κ a (f i) = κ a (s i) := fun i hi ↦ by rw [hf i hi]
  rwa [Finset.prod_congr rfl this, Set.iInter₂_congr hf]

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