English
IndepSets holds for the union s1 ∪ s2 if and only if it holds for s1 and for s2 separately.
Русский
IndepSets выполняется для объединения s1 ∪ s2 тогда и только тогда, когда он выполняется отдельно для s1 и для s2.
LaTeX
$$IndepSets(s1 ∪ s2, s', κ, μ) ↔ (IndepSets(s1, s', κ, μ) ∧ IndepSets(s2, s', κ, μ))$$
Lean4
@[simp]
theorem union_iff {s₁ s₂ s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω} {κ : Kernel α Ω} {μ : Measure α} :
IndepSets (s₁ ∪ s₂) s' κ μ ↔ IndepSets s₁ s' κ μ ∧ IndepSets s₂ s' κ μ :=
⟨fun h =>
⟨indepSets_of_indepSets_of_le_left h Set.subset_union_left,
indepSets_of_indepSets_of_le_left h Set.subset_union_right⟩,
fun h => IndepSets.union h.left h.right⟩