Symmetric_Difference_of_Unions

Proved

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

proofwikiset-unionsymmetric-difference

Let R, S and T be sets. Then (R ∪ T) △ (S ∪ T) = (R △ S) \ T.

Preamble

import Mathlib.Order.SymmDiff
import Mathlib.Data.Set.Basic

Formal statement

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

Source