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