union — Mathlib

English

If CondIndepSets holds for s1 with respect to s' and for s2 with respect to s', then it holds for their union s1 ∪ s2 with respect to s'.

Русский

Если независимость выполняется для s1 относительно s' и для s2 относительно s', то она выполняется и для их объединения s1 ∪ s2 относительно s'.

LaTeX

$$$h_1 : CondIndepSets\, m' hm'\, s_1\, s' μ \\;\\wedge\\; h_2 : CondIndepSets\, m' hm'\, s_2\, s' μ \\Rightarrow CondIndepSets\, m' hm'\, (s_1 \\cup s_2)\, s' μ$$$

Lean4

theorem union {s₁ s₂ s' : Set (Set Ω)} (h₁ : CondIndepSets m' hm' s₁ s' μ) (h₂ : CondIndepSets m' hm' s₂ s' μ) :
    CondIndepSets m' hm' (s₁ ∪ s₂) s' μ :=
  Kernel.IndepSets.union h₁ h₂

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