Grace/Cumulus/Topology/CantorBendixson/Theorem.g17

Open in Workbench Download source

Imports

Stabilise

Declarations

Source

1-- The Cantor–Bendixson theorem: in a space with a countable base, a2-- closed set is the disjoint union of its perfect kernel and a countable3-- set of removed points, and its Cantor–Bendixson rank is countable4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.Topology.CantorBendixson.Theorem10import Stabilise1112-- A perfect set is closed and equal to its derived set: closed with no13-- isolated points.14predicate Perfect (X T P : Set) := IsClosed(X, T, P) ∧ derivedSet(X, T, P) = P1516theorem Perfect.closed (X T P : Set)17  requires perfect : Perfect(X, T, P)18  shows IsClosed(X, T, P)19proof20  exact perfect.left2122theorem Perfect.no_isolated_point (X T P x : Set)23  requires topology : IsTopology(X, T)24  requires perfect : Perfect(X, T, P)25  requires hx : x ∈ P26  shows ¬IsolatedPoint(X, T, P, x)27proof28  obtain ⟨closed, fixed⟩ := perfect29  intro isolated30  have removed := derivedSet.removed_iff.backward with31    topology, closed.left, isolated32  have parts := difference.membership.forward with removed33  apply parts.right34  rw fixed35  exact parts.left3637-- The perfect kernel is perfect: it is a stage, hence closed, and its38-- derived set is the next stage, which is the same set.39theorem cantorBendixson.kernel_perfect (X T B A : Set)40  requires topology : IsTopology(X, T)41  requires basis : Basis(X, T, B)42  requires closed : IsClosed(X, T, A)43  requires countable : Countable(B)44  shows Perfect(X, T, perfectKernel(X, T, A))45proof46  have same : perfectKernel(X, T, A) =47      derived(X, T, A, cantorBendixsonRank(X, T, A))48    unfold perfectKernel49    rfl50  have hRank := cantorBendixsonRank.ordinal with51    topology, basis, closed, countable52  have fixed := cantorBendixsonRank.fixed with53    topology, basis, closed, countable54  rw derived.next at fixed55  rw same at fixed56  rw same57  constructor58  . exact derived.closed with topology, closed, hRank59  . exact fixed6061theorem cantorBendixson.kernel_subset (X T B A : Set)62  requires topology : IsTopology(X, T)63  requires basis : Basis(X, T, B)64  requires closed : IsClosed(X, T, A)65  requires countable : Countable(B)66  shows perfectKernel(X, T, A) ⊆ A67proof68  have hRank := cantorBendixsonRank.ordinal with69    topology, basis, closed, countable70  unfold perfectKernel71  exact derived.subset with topology, closed, hRank7273-- The points removed below stage ρ, each related to the basic sets that74-- witness its removal at the stage where it leaves.75def pointDrops (X T A B ρ : Set) : Set :=76  { p ∈ (A ∖ derived(X, T, A, ρ)) × B |77    ∃ x ∈ A ∖ derived(X, T, A, ρ), ∃ W ∈ B, p = (x ↦ W) ∧78      (∃ β ∈ ρ, W ∩ derived(X, T, A, β) = {x}) }7980theorem pointDrops.relates (X T A B ρ x W : Set)81  shows relates(pointDrops(X, T, A, B, ρ), x, W) ↔82    x ∈ A ∖ derived(X, T, A, ρ) ∧ W ∈ B ∧83      (∃ β ∈ ρ, W ∩ derived(X, T, A, β) = {x})84proof85  constructor86  . intro edge87    unfold relates at edge88    have parts := pointDrops.membership.forward with edge89    obtain ⟨x2, hx2, W2, hW2, shape, witnessed⟩ := parts.right90    obtain ⟨rfl, rfl⟩ := orderedPair.injective with shape91    exact ⟨hx2, hW2, witnessed⟩92  . intro h93    obtain ⟨hx, hW, witnessed⟩ := h94    unfold relates95    apply pointDrops.membership.backward96    constructor97    . exact product.pair with hx, hW98    . exact ⟨x, hx, W, hW, rfl, witnessed⟩99100-- Every removed point has a witness: it leaves at a successor stage below101-- ρ, where a basic set isolates it.102theorem pointDrops.offered (X T A B ρ : Set)103  requires topology : IsTopology(X, T)104  requires basis : Basis(X, T, B)105  requires closed : IsClosed(X, T, A)106  requires hRho : ρ ∈ Ordinal107  shows ∀ x ∈ A ∖ derived(X, T, A, ρ), ∃ W ∈ B,108    relates(pointDrops(X, T, A, B, ρ), x, W)109proof110  intros x hx111  have parts := difference.membership.forward with hx112  obtain ⟨β, hβ, inBeta, away⟩ := derived.removed_stage with113    topology, closed, hRho, parts.left, parts.right114  have hBeta := Ordinal.member with hRho, hβ115  obtain ⟨W, hW, trace⟩ := derived.removed_witness with116    topology, basis, closed, hBeta, inBeta, away117  witness W118  constructor119  . exact hW120  . apply pointDrops.relates.backward121    exact ⟨hx, hW, β, hβ, trace⟩122123-- A basic set witnesses the removal of at most one point.124theorem pointDrops.separated (X T A B ρ : Set)125  requires topology : IsTopology(X, T)126  requires basis : Basis(X, T, B)127  requires closed : IsClosed(X, T, A)128  requires hRho : ρ ∈ Ordinal129  shows ∀ x ∈ A ∖ derived(X, T, A, ρ), ∀ y ∈ A ∖ derived(X, T, A, ρ),130    ∀ W ∈ B, relates(pointDrops(X, T, A, B, ρ), x, W) →131      relates(pointDrops(X, T, A, B, ρ), y, W) → x = y132proof133  intros x hx y hy W hW first second134  obtain ⟨hx2, hW2, β, hβ, traceX⟩ := pointDrops.relates.forward with135    first136  obtain ⟨hy2, hW3, δ, hδ, traceY⟩ := pointDrops.relates.forward with137    second138  have hBeta := Ordinal.member with hRho, hβ139  have hDelta := Ordinal.member with hRho, hδ140  have both := derived.witness_injective with141    topology, basis, closed, hBeta, hDelta, hW, traceX, traceY142  exact both.right143144-- The points removed below any stage are countable: each selects the145-- witness of least code, injectively into the base.146theorem derived.removed_countable (X T A B ρ : Set)147  requires topology : IsTopology(X, T)148  requires basis : Basis(X, T, B)149  requires closed : IsClosed(X, T, A)150  requires countable : Countable(B)151  requires hRho : ρ ∈ Ordinal152  shows Countable(A ∖ derived(X, T, A, ρ))153proof154  obtain ⟨g, code⟩ := countable155  have offered := pointDrops.offered with topology, basis, closed, hRho156  have separated := pointDrops.separated with topology, basis, closed, hRho157  exact leastCoded.countable with code, offered, separated158159theorem cantorBendixson.scattered_countable (X T B A : Set)160  requires topology : IsTopology(X, T)161  requires basis : Basis(X, T, B)162  requires closed : IsClosed(X, T, A)163  requires countable : Countable(B)164  shows Countable(A ∖ perfectKernel(X, T, A))165proof166  have hRank := cantorBendixsonRank.ordinal with167    topology, basis, closed, countable168  unfold perfectKernel169  exact derived.removed_countable with170    topology, basis, closed, countable, hRank171172-- The rank is countable: every stage below it drops, so the stages below173-- the rank select witnesses injectively into the base.174theorem cantorBendixson.rank_countable (X T B A : Set)175  requires topology : IsTopology(X, T)176  requires basis : Basis(X, T, B)177  requires closed : IsClosed(X, T, A)178  requires countable : Countable(B)179  shows Countable(cantorBendixsonRank(X, T, A))180proof181  obtain ⟨g, code⟩ := countable182  have countableB : Countable(B) := ⟨g, code⟩183  have hRank := cantorBendixsonRank.ordinal with184    topology, basis, closed, countableB185  have ordinals : ∀ γ ∈ cantorBendixsonRank(X, T, A), γ ∈ Ordinal186    intros γ hγ187    exact Ordinal.member with hRank, hγ188  have offered : ∀ γ ∈ cantorBendixsonRank(X, T, A), ∃ W ∈ B,189      relates(stageDrops(X, T, A, B, cantorBendixsonRank(X, T, A)), γ, W)190    intros γ hγ191    have hGamma := ordinals with γ, hγ192    have strict : derived(X, T, A, next(γ)) ≠ derived(X, T, A, γ)193      intro stable194      have below := cantorBendixsonRank.least with195        topology, basis, closed, countableB, hGamma, stable196      exact Ordinal.not_member_of_subset with below, hγ197    obtain ⟨W, hW, x, trace⟩ := stageDrops.offered with198      topology, basis, closed, hGamma, strict199    witness W200    constructor201    . exact hW202    . apply stageDrops.relates.backward203      exact ⟨hγ, hW, x, trace⟩204  have separated := stageDrops.separated with topology, basis, closed, ordinals205  exact leastCoded.countable with code, offered, separated206207-- Cantor–Bendixson: a closed set in a space with a countable base is the208-- disjoint union of its perfect kernel and a countable set.209theorem cantorBendixson (X T B A : Set)210  requires topology : IsTopology(X, T)211  requires basis : Basis(X, T, B)212  requires closed : IsClosed(X, T, A)213  requires countable : Countable(B)214  shows Perfect(X, T, perfectKernel(X, T, A)) ∧215    perfectKernel(X, T, A) ⊆ A ∧ Countable(A ∖ perfectKernel(X, T, A))216proof217  refine ⟨?_, ?_, ?_⟩218  . exact cantorBendixson.kernel_perfect with topology, basis, closed, countable219  . exact cantorBendixson.kernel_subset with topology, basis, closed, countable220  . exact cantorBendixson.scattered_countable with221      topology, basis, closed, countable222