bUnion — Mathlib

English

If every s_n for n in a finite index set u is independent with s′, then the union over n ∈ u is independent with s′.

Русский

Если для всех n в конечном наборе индексов u независимы s_n с s′, то объединение по n ∈ u также независимо по отношению к s′.

LaTeX

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

Lean4

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

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