Theorems · Theorem · general topology

CantorBendixson.perfectKernel_eq_iteratedDerivedSet_of_mem_fixedPoints

∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {a : Ordinal.{u}},
  CantorBendixson.iteratedDerivedSet s a ∈ Function.fixedPoints ⇑relDerivedSet →
    CantorBendixson.perfectKernel s = CantorBendixson.iteratedDerivedSet s a

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

Defined in

Mathlib.Topology.CantorBendixson

Cited by

1 results in Mathlib

Foundations

Depth 65 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace