English
The coborder is the complement of closure(s) \ s, equivalently the union of s and the complement of the boundary. It is the largest set in which s is closed; s is locally closed iff coborder(s) is open.
Русский
Coborder(s) есть комплемент closure(s) \ s, эквивалентно объединению s и комплемента границы. Это наибольшее множество, в котором s замкнуто; s локально замкнуто тогда и только тогда, когда coborder(s) открыто.
LaTeX
$$$\operatorname{coborder}(s) = (\operatorname{closure}(s) \setminus s)^c$$$
Lean4
/-- The coborder is defined as the complement of `closure s \ s`,
or the union of `s` and the complement of `∂(s)`.
This is the largest set in which `s` is closed, and `s` is locally closed if and only if
`coborder s` is open.
This is unnamed in the literature, and this name is due to the fact that `coborder s = (border sᶜ)ᶜ`
where `border s = s \ interior s` is the border in the sense of Hausdorff.
-/
def coborder (s : Set X) : Set X :=
(closure s \ s)ᶜ
