Grace/Cumulus/Topology/CantorBendixson/Stabilise.g17

Open in Workbench Download source

Imports

Iterate · Cardinal · Topology.Basis

Declarations

Source

1-- Stabilisation of the derived stages: a point removed at a stage is2-- witnessed by a basic open set, one basic set witnesses at most one3-- removal, so in a space with a countable base the stages stabilise below4-- the Hartogs bound of the base; the Cantor–Bendixson rank is the least5-- stable stage and the perfect kernel is the stage there6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.Topology.CantorBendixson.Stabilise12import Iterate13import Cardinal14import Topology.Basis1516-- A point removed at stage α is isolated in that stage, and a basic open17-- set around it meets the stage only in the point.18theorem derived.removed_witness (X T A B α x : Set)19  requires topology : IsTopology(X, T)20  requires basis : Basis(X, T, B)21  requires closed : IsClosed(X, T, A)22  requires hAlpha : α ∈ Ordinal23  requires hx : x ∈ derived(X, T, A, α)24  requires away : ¬x ∈ derived(X, T, A, next(α))25  shows ∃ W ∈ B, W ∩ derived(X, T, A, α) = {x}26proof27  have closedStage := derived.closed with topology, closed, hAlpha28  have whole := closedStage.left29  rw derived.next at away30  have removed : x ∈ derived(X, T, A, α) ∖ derivedSet(X, T, derived(X, T, A, α))31    exact difference.membership.backward with ⟨hx, away⟩32  have isolated := derivedSet.removed_iff.forward with topology, whole, removed33  obtain ⟨hxStage, U, hU, hxU, trace⟩ := isolated34  obtain ⟨W, hW, hxW, below⟩ := Basis.refine with basis, hU, hxU35  witness W36  constructor37  . exact hW38  . apply Subset.antisymmetric39    . intros y hy40      have parts := intersection.membership.forward with hy41      have inU : y ∈ U ∩ derived(X, T, A, α)42        exact intersection.membership.backward with ⟨(below with43          y, parts.left), parts.right⟩44      rw trace at inU45      exact inU46    . intros y hy47      have same := singleton.membership.forward with hy48      rw same49      exact intersection.membership.backward with ⟨hxW, hx⟩5051-- Conversely a basic set meeting stage α exactly in x removes x at α.52theorem derived.witness_removed (X T A B α x W : Set)53  requires topology : IsTopology(X, T)54  requires basis : Basis(X, T, B)55  requires closed : IsClosed(X, T, A)56  requires hAlpha : α ∈ Ordinal57  requires hW : W ∈ B58  requires trace : W ∩ derived(X, T, A, α) = {x}59  shows x ∈ derived(X, T, A, α) ∧ ¬x ∈ derived(X, T, A, next(α))60proof61  have closedStage := derived.closed with topology, closed, hAlpha62  have whole := closedStage.left63  have self : x ∈ W ∩ derived(X, T, A, α)64    rw trace65    exact singleton.self at x66  have parts := intersection.membership.forward with self67  have openW := Basis.subset with basis, W, hW68  have isolated : IsolatedPoint(X, T, derived(X, T, A, α), x)69    exact ⟨parts.right, W, openW, parts.left, trace⟩70  have removed := derivedSet.removed_iff.backward with topology, whole, isolated71  have removedParts := difference.membership.forward with removed72  constructor73  . exact parts.right74  . rw derived.next75    exact removedParts.right7677-- One basic set cannot witness a removal at two stages: a point removed78-- at the later stage δ lies in every stage up to next(γ), so it is the79-- point removed at γ, which is not in stage next(γ).80theorem derived.witness_below (X T A B γ δ x y W : Set)81  requires topology : IsTopology(X, T)82  requires basis : Basis(X, T, B)83  requires closed : IsClosed(X, T, A)84  requires hGamma : γ ∈ Ordinal85  requires hDelta : δ ∈ Ordinal86  requires less : γ ∈ δ87  requires hW : W ∈ B88  requires first : W ∩ derived(X, T, A, γ) = {x}89  requires second : W ∩ derived(X, T, A, δ) = {y}90  shows ⊥91proof92  have removed := derived.witness_removed with93    topology, basis, closed, hGamma, hW, first94  have hNext := Ordinal.next with hGamma95  have nextBelow := Ordinal.member_iff_next_subset.forward with96    hGamma, hDelta, less97  have bound := Ordinal.subset_bound with hNext, hDelta, nextBelow98  have toNext := derived.decreasing with topology, closed, hNext, hDelta, bound99  have toGamma := derived.antitone with topology, closed, hGamma, hDelta, less100  have selfY : y ∈ W ∩ derived(X, T, A, δ)101    rw second102    exact singleton.self at y103  have partsY := intersection.membership.forward with selfY104  have yNext := toNext with y, partsY.right105  have yGamma := toGamma with y, partsY.right106  have yTrace : y ∈ W ∩ derived(X, T, A, γ)107    exact intersection.membership.backward with ⟨partsY.left, yGamma⟩108  rw first at yTrace109  have same := singleton.membership.forward with yTrace110  rw same at yNext111  exact removed.right with yNext112113theorem derived.witness_injective (X T A B γ δ x y W : Set)114  requires topology : IsTopology(X, T)115  requires basis : Basis(X, T, B)116  requires closed : IsClosed(X, T, A)117  requires hGamma : γ ∈ Ordinal118  requires hDelta : δ ∈ Ordinal119  requires hW : W ∈ B120  requires first : W ∩ derived(X, T, A, γ) = {x}121  requires second : W ∩ derived(X, T, A, δ) = {y}122  shows γ = δ ∧ x = y123proof124  have split := Ordinal.trichotomy with hGamma, δ, hDelta125  have same : γ = δ126    cases split with less | rest127    . exfalso128      exact derived.witness_below with129        topology, basis, closed, hGamma, hDelta, less, hW, first, second130    . cases rest with equal | greater131      . exact equal132      . exfalso133        exact derived.witness_below with134          topology, basis, closed, hDelta, hGamma, greater, hW, second, first135  constructor136  . exact same137  . rw same at first138    rw first at second139    have hx : x ∈ {y}140      rw ← second141      exact singleton.self at x142    exact singleton.membership.forward with hx143144-- The drops of the stages indexed by D: a stage γ ∈ D is related to the145-- basic sets that witness a removal at γ.146def stageDrops (X T A B D : Set) : Set :=147  { p ∈ D × B | ∃ γ ∈ D, ∃ W ∈ B, p = (γ ↦ W) ∧148    (∃ x, W ∩ derived(X, T, A, γ) = {x}) }149150theorem stageDrops.relates (X T A B D γ W : Set)151  shows relates(stageDrops(X, T, A, B, D), γ, W) ↔152    γ ∈ D ∧ W ∈ B ∧ (∃ x, W ∩ derived(X, T, A, γ) = {x})153proof154  constructor155  . intro edge156    unfold relates at edge157    have parts := stageDrops.membership.forward with edge158    obtain ⟨γ2, hγ2, W2, hW2, shape, witnessed⟩ := parts.right159    obtain ⟨rfl, rfl⟩ := orderedPair.injective with shape160    exact ⟨hγ2, hW2, witnessed⟩161  . intro h162    obtain ⟨hγ, hW, witnessed⟩ := h163    unfold relates164    apply stageDrops.membership.backward165    constructor166    . exact product.pair with hγ, hW167    . exact ⟨γ, hγ, W, hW, rfl, witnessed⟩168169theorem stageDrops.separated (X T A B D : Set)170  requires topology : IsTopology(X, T)171  requires basis : Basis(X, T, B)172  requires closed : IsClosed(X, T, A)173  requires ordinals : ∀ γ ∈ D, γ ∈ Ordinal174  shows ∀ γ ∈ D, ∀ δ ∈ D, ∀ W ∈ B,175    relates(stageDrops(X, T, A, B, D), γ, W) →176      relates(stageDrops(X, T, A, B, D), δ, W) → γ = δ177proof178  intros γ hγ δ hδ W hW first second179  obtain ⟨hγ2, hW2, x, traceX⟩ := stageDrops.relates.forward with first180  obtain ⟨hδ2, hW3, y, traceY⟩ := stageDrops.relates.forward with second181  have hGamma := ordinals with γ, hγ182  have hDelta := ordinals with δ, hδ183  have both := derived.witness_injective with184    topology, basis, closed, hGamma, hDelta, hW, traceX, traceY185  exact both.left186187-- A stage that is not stable removes a point, witnessed by a basic set.188theorem stageDrops.offered (X T A B γ : Set)189  requires topology : IsTopology(X, T)190  requires basis : Basis(X, T, B)191  requires closed : IsClosed(X, T, A)192  requires hGamma : γ ∈ Ordinal193  requires strict : derived(X, T, A, next(γ)) ≠ derived(X, T, A, γ)194  shows ∃ W ∈ B, ∃ x, W ∩ derived(X, T, A, γ) = {x}195proof196  have drop := derived.next_subset with topology, closed, hGamma197  have removed : ∃ x ∈ derived(X, T, A, γ),198      ¬x ∈ derived(X, T, A, next(γ))199    by_contra none200    apply strict201    apply Subset.antisymmetric with drop202    intros x hx203    by_contra outside204    apply none205    exact ⟨x, hx, outside⟩206  obtain ⟨x, hx, away⟩ := removed207  obtain ⟨W, hW, trace⟩ := derived.removed_witness with208    topology, basis, closed, hGamma, hx, away209  exact ⟨W, hW, x, trace⟩210211-- Stabilisation: if every stage below the Hartogs bound of the base212-- dropped, the least-coded witnesses would inject the Hartogs bound into213-- the base.214theorem derived.stabilises (X T A B : Set)215  requires topology : IsTopology(X, T)216  requires basis : Basis(X, T, B)217  requires closed : IsClosed(X, T, A)218  requires countable : Countable(B)219  shows ∃ γ ∈ hartogsBound(B),220    derived(X, T, A, next(γ)) = derived(X, T, A, γ)221proof222  obtain ⟨g, code⟩ := countable223  by_contra none224  have hBound := hartogsBound.ordinal at B225  have ordinals : ∀ γ ∈ hartogsBound(B), γ ∈ Ordinal226    intros γ hγ227    exact Ordinal.member with hBound, hγ228  have offered : ∀ γ ∈ hartogsBound(B), ∃ W ∈ B,229      relates(stageDrops(X, T, A, B, hartogsBound(B)), γ, W)230    intros γ hγ231    have hGamma := ordinals with γ, hγ232    have strict : derived(X, T, A, next(γ)) ≠ derived(X, T, A, γ)233      intro equal234      apply none235      exact ⟨γ, hγ, equal⟩236    obtain ⟨W, hW, x, trace⟩ := stageDrops.offered with237      topology, basis, closed, hGamma, strict238    witness W239    constructor240    . exact hW241    . apply stageDrops.relates.backward242      exact ⟨hγ, hW, x, trace⟩243  have separated := stageDrops.separated with topology, basis, closed, ordinals244  have injective := leastCoded.injective with code, offered, separated245  exact hartogsBound.no_injection with injective246247-- Once two consecutive stages agree, every later stage is the same set.248theorem derived.stable_below (X T A γ ε : Set)249  requires topology : IsTopology(X, T)250  requires closed : IsClosed(X, T, A)251  requires hGamma : γ ∈ Ordinal252  requires hEpsilon : ε ∈ Ordinal253  requires stable : derived(X, T, A, next(γ)) = derived(X, T, A, γ)254  shows ∀ δ ∈ next(ε), γ ∈ next(δ) →255    derived(X, T, A, δ) = derived(X, T, A, γ)256proof257  have hNext := Ordinal.next with hEpsilon258  have transitive := Ordinal.transitive with hNext259  have unfolded := stable260  rw derived.next at unfolded261  induction δ over next(ε) ordered by membershipOn(next(ε)) certified by membershipOn.wellFounded at next(ε)262  intros current hCurrentIn ih hBound263  have hCurrent := Ordinal.member with hNext, hCurrentIn264  have bound := next.membership.forward with hBound265  cases bound with earlier | equal266  . have split := Ordinal.cases with hCurrent267    cases split with zero | rest268    . exfalso269      rw zero at earlier270      exact set.empty with earlier271    . cases rest with successor | limit272      . obtain ⟨β, hβ, equalNext⟩ := successor273        have hBeta := Ordinal.member with hCurrent, hβ274        have hBetaIn := transitive with current, hCurrentIn, β, hβ275        have rule := membershipOn.relates with hBetaIn, hCurrentIn276        have predecessor : β ∈ next(ε) ∧277            relates(membershipOn(next(ε)), β, current)278          exact ⟨hBetaIn, (rule.backward with hβ)⟩279        rw ← equalNext at earlier280        have same := ih with β, predecessor, earlier281        rw [← equalNext, derived.next, same]282        exact unfolded283      . have equation := derived.limit at X, T, A, current with limit284        apply Subset.antisymmetric285        . exact derived.antitone with286            topology, closed, hGamma, hCurrent, earlier287        . rw equation288          have stage := derived.stage_in_range at X, T, A with earlier289          have inhabited : Nonempty(Relation.range(derived.history(X, T, A, current)))290            exact ⟨derived(X, T, A, γ), stage⟩291          apply familyIntersection.greatest with inhabited292          intros S hS293          obtain ⟨β, hβ, shape⟩ := derived.history_range.forward with hS294          rw shape295          have hBeta := Ordinal.member with hCurrent, hβ296          have order := Ordinal.trichotomy with hBeta, γ, hGamma297          cases order with less | rest298          . exact derived.antitone with topology, closed, hBeta, hGamma, less299          . cases rest with sameStage | greater300            . rw sameStage301              exact Subset.reflexive302            . have hBetaIn := transitive with current, hCurrentIn, β, hβ303              have rule := membershipOn.relates with hBetaIn, hCurrentIn304              have predecessor : β ∈ next(ε) ∧305                  relates(membershipOn(next(ε)), β, current)306                exact ⟨hBetaIn, (rule.backward with hβ)⟩307              have boundBeta : γ ∈ next(β)308                apply next.membership.backward309                left310                exact greater311              have same := ih with β, predecessor, boundBeta312              rw same313              exact Subset.reflexive314  . rw equal315    rfl316317theorem derived.stable_after (X T A γ δ : Set)318  requires topology : IsTopology(X, T)319  requires closed : IsClosed(X, T, A)320  requires hGamma : γ ∈ Ordinal321  requires hDelta : δ ∈ Ordinal322  requires stable : derived(X, T, A, next(γ)) = derived(X, T, A, γ)323  requires hBound : γ ∈ next(δ)324  shows derived(X, T, A, δ) = derived(X, T, A, γ)325proof326  have below := derived.stable_below at X, T, A, γ, δ with327    topology, closed, hGamma, hDelta, stable328  exact below with δ, (next.contains at δ), hBound329330-- A point of A outside stage ρ is removed at some successor stage below331-- ρ: at the least stage it has left, which is neither zero nor a limit.332333def leftStages (X T A ρ x : Set) : Set :=334  { α ∈ next(ρ) | ¬x ∈ derived(X, T, A, α) }335336theorem derived.removed_stage (X T A ρ x : Set)337  requires topology : IsTopology(X, T)338  requires closed : IsClosed(X, T, A)339  requires hRho : ρ ∈ Ordinal340  requires hx : x ∈ A341  requires away : ¬x ∈ derived(X, T, A, ρ)342  shows ∃ β ∈ ρ,343    x ∈ derived(X, T, A, β) ∧ ¬x ∈ derived(X, T, A, next(β))344proof345  have hNext := Ordinal.next with hRho346  have transitive := Ordinal.transitive with hNext347  have ordinals : ∀ α ∈ leftStages(X, T, A, ρ, x), α ∈ Ordinal348    intros α hα349    have parts := leftStages.membership.forward with hα350    exact Ordinal.member with hNext, parts.left351  have member : ρ ∈ leftStages(X, T, A, ρ, x)352    exact leftStages.membership.backward with ⟨(next.contains at ρ), away⟩353  have inhabited : Nonempty(leftStages(X, T, A, ρ, x)) := ⟨ρ, member⟩354  have nonempty := Nonempty.ne_empty with inhabited355  obtain ⟨m, hm, least⟩ := Ordinal.least with ordinals, nonempty356  have parts := leftStages.membership.forward with hm357  have mIn := parts.left358  have mAway := parts.right359  have hM := Ordinal.member with hNext, mIn360  have split := Ordinal.cases with hM361  cases split with zero | rest362  . exfalso363    apply mAway364    rw [zero, ← nat.zero, derived.zero]365    exact hx366  . cases rest with successor | limit367    . obtain ⟨β, hβ, equalNext⟩ := successor368      have hBetaIn := transitive with m, mIn, β, hβ369      have hBetaRho : β ∈ ρ370        have order := next.membership.forward with hBetaIn371        cases order with less | same372        . exact less373        . exfalso374          rw same at equalNext375          rw ← equalNext at mIn376          exact membership.irreflexive with mIn377      have inBeta : x ∈ derived(X, T, A, β)378        by_contra outside379        have memberBeta : β ∈ leftStages(X, T, A, ρ, x)380          exact leftStages.membership.backward with ⟨hBetaIn, outside⟩381        have below := least with β, memberBeta382        exact Ordinal.not_member_of_subset with below, hβ383      refine ⟨β, hBetaRho, inBeta, ?_⟩384      rw equalNext385      exact mAway386    . exfalso387      have membership := derived.limit_membership at X, T, A, x, m with limit388      apply mAway389      apply membership.backward390      intros β hβ391      by_contra outside392      have hBetaIn := transitive with m, mIn, β, hβ393      have memberBeta : β ∈ leftStages(X, T, A, ρ, x)394        exact leftStages.membership.backward with ⟨hBetaIn, outside⟩395      have below := least with β, memberBeta396      exact Ordinal.not_member_of_subset with below, hβ397398-- The Cantor–Bendixson rank: the least stable stage. The stable stages399-- are collected below the Hartogs bound of the topology, which contains400-- the Hartogs bound of every base; the rank is their intersection, the401-- least of them. The perfect kernel is the stage at the rank.402403def stableStages (X T A : Set) : Set :=404  { γ ∈ hartogsBound(T) | derived(X, T, A, next(γ)) = derived(X, T, A, γ) }405406def cantorBendixsonRank (X T A : Set) : Set := ⋂(stableStages(X, T, A))407408def perfectKernel (X T A : Set) : Set :=409  derived(X, T, A, cantorBendixsonRank(X, T, A))410411theorem stableStages.ordinal (X T A γ : Set)412  requires hγ : γ ∈ stableStages(X, T, A)413  shows γ ∈ Ordinal414proof415  have parts := stableStages.membership.forward with hγ416  exact Ordinal.member with (hartogsBound.ordinal at T), parts.left417418theorem stableStages.nonempty (X T A B : Set)419  requires topology : IsTopology(X, T)420  requires basis : Basis(X, T, B)421  requires closed : IsClosed(X, T, A)422  requires countable : Countable(B)423  shows stableStages(X, T, A) ≠ ∅424proof425  obtain ⟨γ, hγ, stable⟩ := derived.stabilises with426    topology, basis, closed, countable427  have inside := Basis.subset with basis428  have grows := hartogsBound.monotone with inside429  have inT := grows with γ, hγ430  have member : γ ∈ stableStages(X, T, A)431    exact stableStages.membership.backward with ⟨inT, stable⟩432  have inhabited : Nonempty(stableStages(X, T, A)) := ⟨γ, member⟩433  exact Nonempty.ne_empty with inhabited434435theorem cantorBendixsonRank.stable (X T A B : Set)436  requires topology : IsTopology(X, T)437  requires basis : Basis(X, T, B)438  requires closed : IsClosed(X, T, A)439  requires countable : Countable(B)440  shows cantorBendixsonRank(X, T, A) ∈ stableStages(X, T, A)441proof442  have nonempty := stableStages.nonempty with topology, basis, closed, countable443  have ordinals : ∀ γ ∈ stableStages(X, T, A), γ ∈ Ordinal444    intros γ hγ445    exact stableStages.ordinal with hγ446  have least := Ordinal.intersection_least with ordinals, nonempty447  unfold cantorBendixsonRank448  exact least.left449450theorem cantorBendixsonRank.ordinal (X T A B : Set)451  requires topology : IsTopology(X, T)452  requires basis : Basis(X, T, B)453  requires closed : IsClosed(X, T, A)454  requires countable : Countable(B)455  shows cantorBendixsonRank(X, T, A) ∈ Ordinal456proof457  have stable := cantorBendixsonRank.stable with458    topology, basis, closed, countable459  exact stableStages.ordinal with stable460461theorem cantorBendixsonRank.fixed (X T A B : Set)462  requires topology : IsTopology(X, T)463  requires basis : Basis(X, T, B)464  requires closed : IsClosed(X, T, A)465  requires countable : Countable(B)466  shows derived(X, T, A, next(cantorBendixsonRank(X, T, A))) =467    perfectKernel(X, T, A)468proof469  have same : perfectKernel(X, T, A) =470      derived(X, T, A, cantorBendixsonRank(X, T, A))471    unfold perfectKernel472    rfl473  have stable := cantorBendixsonRank.stable with474    topology, basis, closed, countable475  have parts := stableStages.membership.forward with stable476  rw same477  exact parts.right478479theorem cantorBendixsonRank.in_hartogs (X T A B : Set)480  requires topology : IsTopology(X, T)481  requires basis : Basis(X, T, B)482  requires closed : IsClosed(X, T, A)483  requires countable : Countable(B)484  shows cantorBendixsonRank(X, T, A) ∈ hartogsBound(T)485proof486  have stable := cantorBendixsonRank.stable with487    topology, basis, closed, countable488  have parts := stableStages.membership.forward with stable489  exact parts.left490491-- The rank is the least stable ordinal: a stable ordinal below it would492-- be a stable stage below the intersection of the stable stages.493theorem cantorBendixsonRank.least (X T A B γ : Set)494  requires topology : IsTopology(X, T)495  requires basis : Basis(X, T, B)496  requires closed : IsClosed(X, T, A)497  requires countable : Countable(B)498  requires hGamma : γ ∈ Ordinal499  requires stable : derived(X, T, A, next(γ)) = derived(X, T, A, γ)500  shows cantorBendixsonRank(X, T, A) ⊆ γ501proof502  have same : cantorBendixsonRank(X, T, A) = ⋂(stableStages(X, T, A))503    unfold cantorBendixsonRank504    rfl505  have hRank := cantorBendixsonRank.ordinal with506    topology, basis, closed, countable507  have inHartogs := cantorBendixsonRank.in_hartogs with508    topology, basis, closed, countable509  have order := Ordinal.subset_or_member with hRank, hGamma510  cases order with below | above511  . exact below512  . exfalso513    have inside := Ordinal.member_subset with514      (hartogsBound.ordinal at T), inHartogs515    have inT := inside with γ, above516    have member : γ ∈ stableStages(X, T, A)517      exact stableStages.membership.backward with ⟨inT, stable⟩518    have nonempty := stableStages.nonempty with519      topology, basis, closed, countable520    have ordinals : ∀ δ ∈ stableStages(X, T, A), δ ∈ Ordinal521      intros δ hδ522      exact stableStages.ordinal with hδ523    have least := Ordinal.intersection_least with ordinals, nonempty524    have rankBelow := least.right with γ, member525    have rankBelowGamma : cantorBendixsonRank(X, T, A) ⊆ γ526      rw same527      exact rankBelow528    exact Ordinal.not_member_of_subset with rankBelowGamma, above529530-- Every stage from the rank on is the perfect kernel.531theorem perfectKernel.stage (X T A B δ : Set)532  requires topology : IsTopology(X, T)533  requires basis : Basis(X, T, B)534  requires closed : IsClosed(X, T, A)535  requires countable : Countable(B)536  requires hDelta : δ ∈ Ordinal537  requires hBound : cantorBendixsonRank(X, T, A) ∈ next(δ)538  shows derived(X, T, A, δ) = perfectKernel(X, T, A)539proof540  have same : perfectKernel(X, T, A) =541      derived(X, T, A, cantorBendixsonRank(X, T, A))542    unfold perfectKernel543    rfl544  have hRank := cantorBendixsonRank.ordinal with545    topology, basis, closed, countable546  have stable := cantorBendixsonRank.stable with547    topology, basis, closed, countable548  have parts := stableStages.membership.forward with stable549  rw same550  exact derived.stable_after with551    topology, closed, hRank, hDelta, parts.right, hBound552