iUnion — Mathlib

English

If every s_n in a family is independent with s′, then the union of all s_n is independent with s′.

Русский

Если каждый s_n в семье независим с s′, то объединение всех s_n несет независимость с s′.

LaTeX

$$∀ n, IndepSets(s_n, s', κ, μ) ⇒ IndepSets(⋃ n, s_n, s', κ, μ)$$

Lean4

theorem iUnion {s : ι → Set (Set Ω)} {s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
    (hyp : ∀ n, IndepSets (s n) s' κ μ) : IndepSets (⋃ n, s n) s' κ μ :=
  by
  intro t1 t2 ht1 ht2
  rw [Set.mem_iUnion] at ht1
  obtain ⟨n, ht1⟩ := ht1
  exact hyp n t1 t2 ht1 ht2

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