Grace/Cumulus/Topology/CantorBendixson.g17

Open in Workbench Download source

Imports

CantorBendixson.Derived · CantorBendixson.Iterate · CantorBendixson.Stabilise · CantorBendixson.Theorem

Declarations

Source

1-- Cantor–Bendixson: derived sets, their transfinite iteration, the2-- stabilisation of the stages at a countable ordinal, and the theorem3-- that a closed set in a space with a countable base is the disjoint4-- union of a perfect set and a countable set5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Topology.CantorBendixson11import CantorBendixson.Derived12import CantorBendixson.Iterate13import CantorBendixson.Stabilise14import CantorBendixson.Theorem15