Union_of_Symmetric_Differences

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

proofwikiset-theoryset-unionsymmetric-difference

Let R, S, T be sets. Then (R Δ S) ∪ (S Δ T) = (R ∪ S ∪ T) \ (R ∩ S ∩ T).

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Union_of_Symmetric_Differences {α : Type _} (R S T : Set α) : (symmDiff R S) ∪ (symmDiff S T) = (R ∪ S ∪ T) \ (R ∩ S ∩ T) := by sorry

Source