Intersection_is_Associative
Provedassociativitydirect-proofsintersection-is-associativeproofwikiretryset-intersection
Set intersection is associative.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Intersection_is_Associative {α : Type _} (A B C : Set α) : A ∩ (B ∩ C) = (A ∩ B) ∩ C := by sorry