-- Cantor–Bendixson: derived sets, their transfinite iteration, the
-- stabilisation of the stages at a countable ordinal, and the theorem
-- that a closed set in a space with a countable base is the disjoint
-- union of a perfect set and a countable set
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Topology.CantorBendixson
import CantorBendixson.Derived
import CantorBendixson.Iterate
import CantorBendixson.Stabilise
import CantorBendixson.Theorem