Intersection_of_Power_Sets
Provedpower-setproofwikiset-intersection
The intersection of the power sets of two sets S and T is equal to the power set of their intersection: 𝒫(S) ∩ 𝒫(T) = 𝒫(S ∩ T).
Preamble
import Mathlib.Data.Set.Lattice
Formal statement
theorem Intersection_of_Power_Sets {α : Type _} (S T : Set α) : Set.powerset S ∩ Set.powerset T = Set.powerset (S ∩ T) := by sorrySource