Characterization of subsets in topological spaces

Stream: Is there code for X?

[Kin Yau James Wong]

Are there theorems asserting that

$$S = \overline{S} \cap (S \cup \overline{S}^c)$$

where

$$S \cup \overline{S}^c$$

is dense?

[Aaron Liu]

Is this what you want?

import Mathlib

open Set

example {X : Type*} [TopologicalSpace X] {S : Set X} : S = closure S ∩ (S ∪ (closure S)ᶜ) := by
  simp [inter_union_distrib_left, subset_closure]

[Kin Yau James Wong]

Yes, I was wondering if it already existed in Mathlib already - I think it might also be nice to have another lemma stating that the latter set is dense

[Aaron Liu]

I think you want docs#dense_coborder