Naming request

Stream: mathlib4

[Andrew Yang]

What should I call the set

def coborder {α} [TopologicalSpace α] (s : Set α) : Set α :=
(closure s \ s)ᶜ

This is the largest set such that s is closed in, and s is locally closed iff this is open (which is what I need it for).
The current name is due to the fact that it is equal to $\overline{b(\overline{S})}$, with $b(S) = \partial S \cap S$ is the border in the sense of Hausdorff, but is there a more sensible name?

[Yaël Dillies]

Do we not have this already?

[Yaël Dillies]

Ah no, I was confusing with docs#exterior