Union_with_Relative_Complement
Provedproofwikirelative-complementset-union
The union of the relative complement of T in S and T equals S, provided T ⊆ S: (S \ T) ∪ T = S
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Union_with_Relative_Complement {α : Type _} (S T : Set α) (hT : T ⊆ S) : (S \ T) ∪ T = S := by sorrySource