union — Mathlib

English

If two families of sets s1 and s2 are independently distributed with respect to s′, then the union of these families is also independent with respect to s′.

Русский

Если две семьи множеств s1 и s2 независимы по отношению к s′, то их объединение также независимо распределено по отношению к s′.

LaTeX

$$IndepSets(s1, s′, κ, μ) ∧ IndepSets(s2, s′, κ, μ) ⇒ IndepSets(s1 ∪ s2, s′, κ, μ)$$

Lean4

theorem union {s₁ s₂ s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α}
    (h₁ : IndepSets s₁ s' κ μ) (h₂ : IndepSets s₂ s' κ μ) : IndepSets (s₁ ∪ s₂) s' κ μ :=
  by
  intro t1 t2 ht1 ht2
  rcases (Set.mem_union _ _ _).mp ht1 with ht1₁ | ht1₂
  · exact h₁ t1 t2 ht1₁ ht2
  · exact h₂ t1 t2 ht1₂ ht2

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