Cantor–Bendixson derivatives of ordinals

A normal function on the ordinals is a closed topological embedding. Consequently the a-th derivative of the ordinal space consists, apart from stage zero, of the positive multiples of ω ^ a.

theorem Order.IsNormal.isClosedMap {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) : IsClosedMap f

A normal ordinal function is a closed map.

theorem Order.IsNormal.isClosedEmbedding {f : Ordinal.{u} → Ordinal.{u}} (hf : IsNormal f) : Topology.IsClosedEmbedding f

A normal ordinal function is a closed topological embedding.

def Ordinal.positivePrincipalMultiples (a : Ordinal.{u}) : Set Ordinal.{u}

The positive ordinal multiples ω ^ a * q, with q > 0.

Equations

• a.positivePrincipalMultiples = (fun (x : Ordinal.{?u.1}) => Ordinal.omega0 ^ a * x) '' Set.Ioi 0

theorem Ordinal.mem_positivePrincipalMultiples {a x : Ordinal.{u}} : x ∈ a.positivePrincipalMultiples ↔ ∃ q > 0, omega0 ^ a * q = x

Membership in the positive multiples of ω ^ a.

theorem Ordinal.cantorBendixson_top_eq (a : Ordinal.{u}) : ↑(⊤.cantorBendixson a) = if a = 0 then Set.univ else a.positivePrincipalMultiples

The a-th derivative of the ordinal space is the set of positive multiples of ω ^ a, except that stage zero is the whole space.