Grace/Cumulus/Topology/CantorBendixson/Iterate.g17

Open in Workbench Download source

Imports

Derived

Declarations

• derived def
• derived.zero theorem derivation
• derived.next theorem derivation
• derived.limit theorem derivation
• derived.history_membership theorem derivation
• derived.history_range theorem derivation
• derived.stage_in_range theorem derivation
• derived.limit_membership theorem derivation
• derived.closed_below theorem derivation
• derived.closed theorem derivation
• derived.subset_whole theorem derivation
• derived.decreasing_below theorem derivation
• derived.decreasing theorem derivation
• derived.antitone theorem derivation
• derived.next_subset theorem derivation
• derived.subset theorem derivation

Source

1-- The transfinite iteration of the derived set: stages indexed by the2-- ordinals, intersecting at limits, with the three recursion laws, the3-- membership form at limits, and the stages closed and decreasing4-- 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.Iterate10import Derived1112-- The stages of a set A: the set itself, then the derived set of the13-- previous stage, and at a limit the intersection of the earlier stages.14noncomputable transfinite def derived (X T A : Set, α : Ordinal) : Set15  | 0 => A16  | succ β => derivedSet(X, T, derived(X, T, A, β))17  | limit λ => ⋂(Relation.range(history))1819theorem derived.zero (X T A : Set)20  shows derived(X, T, A, 0) = A21proof22  simp [derived, nat.zero]2324theorem derived.next (X T A : Set, α : Ordinal)25  shows derived(X, T, A, next(α)) = derivedSet(X, T, derived(X, T, A, α))26proof27  simp [derived.equation.successor]2829theorem derived.limit (X T A λ : Set)30  requires limit : Limit(λ)31  shows derived(X, T, A, λ) = ⋂(Relation.range(derived.history(X, T, A, λ)))32proof33  simp [derived.equation.limit]3435theorem derived.history_membership (p X T A λ : Set)36  shows p ∈ derived.history(X, T, A, λ) ↔37    ∃ β ∈ λ, p = (β ↦ derived(X, T, A, β))38proof39  simp [derived.history.membership]4041theorem derived.history_range (y X T A λ : Set)42  shows y ∈ Relation.range(derived.history(X, T, A, λ)) ↔43    ∃ β ∈ λ, y = derived(X, T, A, β)44proof45  constructor46  . intro hy47    obtain ⟨β, hPair⟩ := range.membership_iff.forward with hy48    have member : (β, y) ∈ derived.history(X, T, A, λ) := hPair49    obtain ⟨γ, hγ, shape⟩ := derived.history_membership.forward with50      member51    have coordinates := orderedPair.injective with shape52    witness γ53    constructor54    . exact hγ55    . exact coordinates.right56  . intro h57    obtain ⟨β, hβ, shape⟩ := h58    have member : (β ↦ derived(X, T, A, β)) ∈ derived.history(X, T, A, λ)59      exact derived.history_membership.backward with ⟨β, hβ, rfl⟩60    rw shape61    exact range.contains with member6263theorem derived.stage_in_range (X T A β λ : Set)64  requires hβ : β ∈ λ65  shows derived(X, T, A, β) ∈ Relation.range(derived.history(X, T, A, λ))66proof67  exact derived.history_range.backward with ⟨β, hβ, rfl⟩6869-- At a limit, a point lies in the stage exactly when it lies in every70-- earlier stage.71theorem derived.limit_membership (X T A x λ : Set)72  requires limit : Limit(λ)73  shows x ∈ derived(X, T, A, λ) ↔ ∀ β ∈ λ, x ∈ derived(X, T, A, β)74proof75  have equation := derived.limit at X, T, A, λ with limit76  rw equation77  constructor78  . intros hx β hβ79    have parts := familyIntersection.membership.forward with hx80    have stage := derived.stage_in_range at X, T, A with hβ81    exact parts.right with derived(X, T, A, β), stage82  . intro below83    obtain ⟨ordinal, nonzero, successors⟩ := limit84    obtain ⟨β, hβ⟩ := Nonempty.of_ne_empty with nonzero85    have stage := derived.stage_in_range at X, T, A with hβ86    have inhabited : Nonempty(Relation.range(derived.history(X, T, A, λ)))87      exact ⟨derived(X, T, A, β), stage⟩88    apply familyIntersection.membership_of_nonempty.backward with inhabited89    intros S hS90    obtain ⟨γ, hγ, shape⟩ := derived.history_range.forward with hS91    rw shape92    exact below with γ, hγ9394-- Every stage of a closed set is closed: the derived set of a closed set95-- is closed, and so is an intersection of closed sets. The induction runs96-- over the ordinals up to a bound, ordered by membership.97theorem derived.closed_below (X T A β : Set)98  requires topology : IsTopology(X, T)99  requires closed : IsClosed(X, T, A)100  requires hBeta : β ∈ Ordinal101  shows ∀ α ∈ next(β), IsClosed(X, T, derived(X, T, A, α))102proof103  have hNext := Ordinal.next with hBeta104  have transitive := Ordinal.transitive with hNext105  induction α over next(β) ordered by membershipOn(next(β)) certified by membershipOn.wellFounded at next(β)106  intros current hCurrentIn ih107  have hCurrent := Ordinal.member with hNext, hCurrentIn108  have split := Ordinal.cases with hCurrent109  cases split with zero | rest110  . rw [zero, ← nat.zero, derived.zero]111    exact closed112  . cases rest with successor | limit113    . obtain ⟨γ, hγ, equal⟩ := successor114      have hGamma := Ordinal.member with hCurrent, hγ115      have hGammaIn := transitive with current, hCurrentIn, γ, hγ116      have rule := membershipOn.relates with hGammaIn, hCurrentIn117      have predecessor : γ ∈ next(β) ∧118          relates(membershipOn(next(β)), γ, current)119        exact ⟨hGammaIn, (rule.backward with hγ)⟩120      have closedGamma := ih with γ, predecessor121      rw [← equal, derived.next]122      exact derivedSet.closed with topology, closedGamma123    . have equation := derived.limit at X, T, A, current with limit124      rw equation125      obtain ⟨ordinal, nonzero, successors⟩ := limit126      obtain ⟨γ, hγ⟩ := Nonempty.of_ne_empty with nonzero127      have stage := derived.stage_in_range at X, T, A with hγ128      have inhabited : Nonempty(Relation.range(derived.history(X, T, A, current)))129        exact ⟨derived(X, T, A, γ), stage⟩130      apply IsClosed.family_intersection with topology, inhabited131      intros S hS132      obtain ⟨ε, hε, shape⟩ := derived.history_range.forward with hS133      rw shape134      have hEpsilonIn := transitive with current, hCurrentIn, ε, hε135      have rule := membershipOn.relates with hEpsilonIn, hCurrentIn136      have predecessor : ε ∈ next(β) ∧137          relates(membershipOn(next(β)), ε, current)138        exact ⟨hEpsilonIn, (rule.backward with hε)⟩139      exact ih with ε, predecessor140141theorem derived.closed (X T A α : Set)142  requires topology : IsTopology(X, T)143  requires closed : IsClosed(X, T, A)144  requires hAlpha : α ∈ Ordinal145  shows IsClosed(X, T, derived(X, T, A, α))146proof147  have below := derived.closed_below at X, T, A, α with148    topology, closed, hAlpha149  exact below with α, (next.contains at α)150151theorem derived.subset_whole (X T A α : Set)152  requires topology : IsTopology(X, T)153  requires closed : IsClosed(X, T, A)154  requires hAlpha : α ∈ Ordinal155  shows derived(X, T, A, α) ⊆ X156proof157  have closedStage := derived.closed with topology, closed, hAlpha158  exact closedStage.left159160-- The stages decrease along the ordinals: a successor stage is the161-- derived set of a closed stage, which lies inside it, and a limit stage162-- is the intersection of the earlier ones.163theorem derived.decreasing_below (X T A δ : Set)164  requires topology : IsTopology(X, T)165  requires closed : IsClosed(X, T, A)166  requires hDelta : δ ∈ Ordinal167  shows ∀ β ∈ next(δ), ∀ α, α ∈ Ordinal → α ∈ next(β) →168    (derived(X, T, A, β) ⊆ derived(X, T, A, α))169proof170  have hNext := Ordinal.next with hDelta171  have transitive := Ordinal.transitive with hNext172  induction β over next(δ) ordered by membershipOn(next(δ)) certified by membershipOn.wellFounded at next(δ)173  intros current hCurrentIn ih α hAlpha hBound174  have hCurrent := Ordinal.member with hNext, hCurrentIn175  have bound := next.membership.forward with hBound176  cases bound with earlier | equal177  . have split := Ordinal.cases with hCurrent178    cases split with zero | rest179    . exfalso180      rw zero at earlier181      exact set.empty with earlier182    . cases rest with successor | limit183      . obtain ⟨γ, hγ, equal⟩ := successor184        have hGamma := Ordinal.member with hCurrent, hγ185        have hGammaIn := transitive with current, hCurrentIn, γ, hγ186        have rule := membershipOn.relates with hGammaIn, hCurrentIn187        have predecessor : γ ∈ next(δ) ∧188            relates(membershipOn(next(δ)), γ, current)189          exact ⟨hGammaIn, (rule.backward with hγ)⟩190        have closedGamma := derived.closed with topology, closed, hGamma191        rw ← equal at earlier192        have toAlpha := ih with γ, predecessor, α, hAlpha, earlier193        have drop := derivedSet.subset with topology, closedGamma194        rw [← equal, derived.next]195        exact Subset.transitive with drop, toAlpha196      . have equation := derived.limit at X, T, A, current with limit197        rw equation198        have stage := derived.stage_in_range at X, T, A with earlier199        exact familyIntersection.subset_of_member with stage200  . rw equal201    exact Subset.reflexive202203theorem derived.decreasing (X T A α β : Set)204  requires topology : IsTopology(X, T)205  requires closed : IsClosed(X, T, A)206  requires hAlpha : α ∈ Ordinal207  requires hBeta : β ∈ Ordinal208  requires hBound : α ∈ next(β)209  shows derived(X, T, A, β) ⊆ derived(X, T, A, α)210proof211  have below := derived.decreasing_below at X, T, A, β with212    topology, closed, hBeta213  exact below with β, (next.contains at β), α, hAlpha, hBound214215theorem derived.antitone (X T A α β : Set)216  requires topology : IsTopology(X, T)217  requires closed : IsClosed(X, T, A)218  requires hAlpha : α ∈ Ordinal219  requires hBeta : β ∈ Ordinal220  requires hLess : α ∈ β221  shows derived(X, T, A, β) ⊆ derived(X, T, A, α)222proof223  have bound : α ∈ next(β)224    apply next.membership.backward225    left226    exact hLess227  exact derived.decreasing with topology, closed, hAlpha, hBeta, bound228229theorem derived.next_subset (X T A α : Set)230  requires topology : IsTopology(X, T)231  requires closed : IsClosed(X, T, A)232  requires hAlpha : α ∈ Ordinal233  shows derived(X, T, A, next(α)) ⊆ derived(X, T, A, α)234proof235  have closedStage := derived.closed with topology, closed, hAlpha236  rw derived.next237  exact derivedSet.subset with topology, closedStage238239theorem derived.subset (X T A α : Set)240  requires topology : IsTopology(X, T)241  requires closed : IsClosed(X, T, A)242  requires hAlpha : α ∈ Ordinal243  shows derived(X, T, A, α) ⊆ A244proof245  have bound := Ordinal.subset_bound at ∅, α with246    Ordinal.empty, hAlpha, (empty.subset at α)247  have below := derived.decreasing at X, T, A, ∅, α with248    topology, closed, Ordinal.empty, hAlpha, bound249  rw [← nat.zero, derived.zero] at below250  exact below251