Closure_of_Intersection_is_Subset_of_Intersection_of_Closures
Provedproofwikiset-closuresset-intersection
Let be a topological space. Let be an indexing set. Let . Then where denotes the closure of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Closure_of_Intersection_is_Subset_of_Intersection_of_Closures {α : Type _} [TopologicalSpace α] (s t : Set α) : closure (s ∩ t) ⊆ closure s ∩ closure t := by sorrySource