Theorems · Definition · general topology

coborder

{X : Type u} → [TopologicalSpace X] → Set X → Set X

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.

Defined in

Mathlib.Topology.Defs.Basic

Cited by

22 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

TopologicalSpace