(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)
Demostrar con Lean4 que
\[ (s \setminus t) ∪ (t \setminus s) = (s ∪ t) \setminus (s ∩ t) \]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 |
import Mathlib.Data.Set.Basic open Set variable {α : Type} variable (s t : Set α) example : (s \\ t) ∪ (t \\ s) = (s ∪ t) \\ (s ∩ t) := by sorry |