Union_is_Idempotent
Provedidempotenceproofwikiset-union
Set union is idempotent
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Union_is_Idempotent {α : Type*} (S : Set α) : S ∪ S = S := by sorrySource
Set union is idempotent
import Mathlib.Data.Set.Basic
theorem Union_is_Idempotent {α : Type*} (S : Set α) : S ∪ S = S := by sorry