Symmetric_Diff_of_Unions_Subset_Union_of_Symmetric_Diffs
Provedproofwikiset-theoryset-unionsymmetric-difference
The symmetric difference of unions is a subset of the union of symmetric differences.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Symmetric_Diff_of_Unions_Subset_Union_of_Symmetric_Diffs {α : Type _} {ι : Type _} (S T : ι → Set α) : symmDiff (⋃ i, S i) (⋃ i, T i) ⊆ ⋃ i, symmDiff (S i) (T i) := by sorrySource