Cantor-Bendixson derivatives and perfect kernel

This file defines the transfinite iteration of the relative derived-set operator and the associated perfect kernel.

For closed sets, the relative derived set agrees with derivedSet, so this recovers the usual Cantor-Bendixson derivative sequence of a closed set.

Main definitions

• CantorBendixson.iteratedDerivedSet s a: the a-th transfinite iterate of relDerivedSet starting from s.
• CantorBendixson.perfectKernel s: the largest perfect subset of s, defined as the intersection of all iterated derived sets of s.

Main statements

• CantorBendixson.iteratedDerivedSet_constant_iff_preperfect: a set is preperfect if and only if every iterated derived set is equal to the original set.
• CantorBendixson.iteratedDerivedSet_stay: the iterated derived-set sequence eventually stabilizes.
• CantorBendixson.perfect_perfectKernel: the perfect kernel of a closed set is perfect.
• CantorBendixson.subset_perfectKernel_of_perfect: the perfect kernel is the largest perfect subset.

Notation

• sᵈ[a]: the a-th iterated relative derived set of s.

Implementation notes

• We define iteratedDerivedSet using OrdinalApprox.gfpApprox applied to relDerivedSet. This keeps the transfinite sequence antitone for arbitrary sets.
• If s is closed, then relDerivedSet s = derivedSet s, so successor stages agree with the ambient derived-set operator.

TODO

• Pointwise and setwise Cantor-Bendixson ranks.
• A generalized Cantor-Bendixson decomposition theorem for arbitrary topological spaces and arbitrary cardinalities of topological bases.

def CantorBendixson.iteratedDerivedSet {X : Type u} [TopologicalSpace X] (s : Set X) : Ordinal.{u} → Set X

The transfinite iteration of the relative derived-set operator on a set.

Equations

• CantorBendixson.iteratedDerivedSet s = OrdinalApprox.gfpApprox relDerivedSet s

def CantorBendixson.«term_ᵈ[_]» : Lean.TrailingParserDescr

The transfinite iteration of the relative derived-set operator on a set.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CantorBendixson.iteratedDerivedSet_zero {X : Type u} [TopologicalSpace X] {s : Set X} : iteratedDerivedSet s 0 = s

@[simp]

theorem CantorBendixson.iteratedDerivedSet_succ {X : Type u} [TopologicalSpace X] {s : Set X} {a : Ordinal.{u}} : iteratedDerivedSet s (a + 1) = relDerivedSet (iteratedDerivedSet s a)

theorem CantorBendixson.iteratedDerivedSet_limit {X : Type u} [TopologicalSpace X] {s : Set X} {a : Ordinal.{u}} (ha : Order.IsSuccLimit a) : iteratedDerivedSet s a = ⋂ (b : ↑(Set.Iio a)), iteratedDerivedSet s ↑b

theorem CantorBendixson.iteratedDerivedSet_constant_iff_preperfect {X : Type u} [TopologicalSpace X] {s : Set X} : Preperfect s ↔ ∀ (a : Ordinal.{u}), iteratedDerivedSet s a = s

A set is preperfect if and only if every stage of its iterated relative derived-set sequence is equal to the original set.

theorem CantorBendixson.isClosed_iteratedDerivedSet {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) (a : Ordinal.{u}) : IsClosed (iteratedDerivedSet s a)

theorem CantorBendixson.iteratedDerivedSet_antitone {X : Type u} [TopologicalSpace X] (s : Set X) : Antitone (iteratedDerivedSet s)

theorem CantorBendixson.iteratedDerivedSet_mono {X : Type u} [TopologicalSpace X] : Monotone fun (s : Set X) => iteratedDerivedSet s

theorem CantorBendixson.mem_fixedPoints_of_iteratedDerivedSet_succ_eq {X : Type u} [TopologicalSpace X] {s : Set X} {a : Ordinal.{u}} (ha : iteratedDerivedSet s (a + 1) = iteratedDerivedSet s a) : iteratedDerivedSet s a ∈ Function.fixedPoints ⇑relDerivedSet

If the iterated derived set stops changing at a successor stage, then sᵈ[a] is a fixed point of relDerivSet.

theorem CantorBendixson.iteratedDerivedSet_mem_fixedPoints {X : Type u} [TopologicalSpace X] (s : Set X) : ∃ (a : Ordinal.{u}), iteratedDerivedSet s a ∈ Function.fixedPoints ⇑relDerivedSet

def CantorBendixson.perfectKernel {X : Type u} [TopologicalSpace X] (s : Set X) : Set X

The perfect kernel of a set, defined as the intersection of all iterated derived sets. It is the largest perfect subset of the original set.

Equations

• CantorBendixson.perfectKernel s = ⋂ (a : Ordinal.{?u.1}), CantorBendixson.iteratedDerivedSet s a

theorem CantorBendixson.perfectKernel_subset_iteratedDerivedSet {X : Type u} [TopologicalSpace X] (s : Set X) (a : Ordinal.{u}) : perfectKernel s ⊆ iteratedDerivedSet s a

theorem CantorBendixson.perfectKernel_subset {X : Type u} [TopologicalSpace X] (s : Set X) : perfectKernel s ⊆ s

theorem CantorBendixson.perfectKernel_mono {X : Type u} [TopologicalSpace X] {s t : Set X} (hst : s ⊆ t) : perfectKernel s ⊆ perfectKernel t

theorem CantorBendixson.isClosed_perfectKernel {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) : IsClosed (perfectKernel s)

@[simp]

theorem CantorBendixson.perfectKernel_empty {X : Type u} [TopologicalSpace X] : perfectKernel ∅ = ∅

theorem CantorBendixson.perfectKernel_eq_iteratedDerivedSet_of_mem_fixedPoints {X : Type u} [TopologicalSpace X] {s : Set X} {a : Ordinal.{u}} (ha : iteratedDerivedSet s a ∈ Function.fixedPoints ⇑relDerivedSet) : perfectKernel s = iteratedDerivedSet s a

Once sᵈ[a] is a fixed point of relDerivSet, the perfect kernel equals sᵈ[a].

theorem Perfect.subset_perfectKernel {X : Type u} [TopologicalSpace X] {s P : Set X} (hP : Perfect P) (hPs : P ⊆ s) : P ⊆ CantorBendixson.perfectKernel s

Every perfect subset of a set is contained in its perfect kernel.

theorem CantorBendixson.perfect_perfectKernel {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) : Perfect (perfectKernel s)

The perfect kernel of a closed set is perfect.

theorem CantorBendixson.perfectKernel_idem {X : Type u} [TopologicalSpace X] {s : Set X} (hs : IsClosed s) : perfectKernel (perfectKernel s) = perfectKernel s

Taking the perfect kernel of a closed set is idempotent.