union_iff — Mathlib

English

Equivalence for union: CondIndepSets m' hm' (s1 ∪ s2) s' μ is equivalent to CondIndepSets m' hm' s1 s' μ and CondIndepSets m' hm' s2 s' μ.

Русский

Эквивалентность объединения: CondIndepSets m' hm' (s1 ∪ s2) s' μ эквивалентно независимости для s1 и для s2 отдельно.

LaTeX

$$$CondIndepSets\, m' hm' (s_1 \\cup s_2)\\, s'\\, μ \\iff (CondIndepSets\, m' hm'\, s_1\, s' μ) \\land (CondIndepSets\, m' hm'\, s_2\, s' μ)$$$

Lean4

@[simp]
theorem union_iff {s₁ s₂ s' : Set (Set Ω)} :
    CondIndepSets m' hm' (s₁ ∪ s₂) s' μ ↔ CondIndepSets m' hm' s₁ s' μ ∧ CondIndepSets m' hm' s₂ s' μ :=
  Kernel.IndepSets.union_iff

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