Topological_Closure_of_Subset_is_Subset_of_Topological_Closure
Provedproofwikiset-closuressubsetstopological-closure-of-subset-is-subset-of-topological-closure
Let be a topological space. Let and . Then where denotes the closure of .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Topological_Closure_of_Subset_is_Subset_of_Topological_Closure {α : Type _} [TopologicalSpace α] {s t : Set α} (h : s ⊆ t) : closure s ⊆ closure t := by sorrySource