Grace/Cumulus/Topology/Real/CantorBendixson.g17

Open in Workbench Download source

Imports

RationalBase · Topology.CantorBendixson

Declarations

Source

1-- Cantor–Bendixson on the real line: every closed set of reals is the2-- disjoint union of a perfect set and a countable set, through the3-- countable basis of rational intervals4-- 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.Real.CantorBendixson10import RationalBase11import Topology.CantorBendixson1213-- The kernel of a closed set of reals is perfect, lies inside the set,14-- and leaves a countable remainder.15theorem reals.cantorBendixson (A : Set)16  requires closed : IsClosed(ℝ, realTopology, A)17  shows Perfect(ℝ, realTopology, perfectKernel(ℝ, realTopology, A)) ∧18    perfectKernel(ℝ, realTopology, A) ⊆ A ∧19    Countable(A ∖ perfectKernel(ℝ, realTopology, A))20proof21  have topology := realTopology.topology22  have basis := rationalIntervals.basis23  have countable := rationalIntervals.countable24  exact cantorBendixson with topology, basis, closed, countable2526theorem reals.kernel_perfect (A : Set)27  requires closed : IsClosed(ℝ, realTopology, A)28  shows Perfect(ℝ, realTopology, perfectKernel(ℝ, realTopology, A))29proof30  have parts := reals.cantorBendixson with closed31  exact parts.left3233theorem reals.kernel_subset (A : Set)34  requires closed : IsClosed(ℝ, realTopology, A)35  shows perfectKernel(ℝ, realTopology, A) ⊆ A36proof37  obtain ⟨perfect, inside, countable⟩ := reals.cantorBendixson with closed38  exact inside3940theorem reals.scattered_countable (A : Set)41  requires closed : IsClosed(ℝ, realTopology, A)42  shows Countable(A ∖ perfectKernel(ℝ, realTopology, A))43proof44  obtain ⟨perfect, inside, countable⟩ := reals.cantorBendixson with closed45  exact countable4647-- The rank of a closed set of reals is a countable ordinal.48theorem reals.rank_countable (A : Set)49  requires closed : IsClosed(ℝ, realTopology, A)50  shows Countable(cantorBendixsonRank(ℝ, realTopology, A))51proof52  have topology := realTopology.topology53  have basis := rationalIntervals.basis54  have countable := rationalIntervals.countable55  exact cantorBendixson.rank_countable with topology, basis, closed, countable5657-- A closed set of reals is countable or contains a nonempty perfect set:58-- either the kernel is empty and the set is its countable remainder, or59-- the kernel is the perfect part.60theorem closed.countable_or_perfect_part (A : Set)61  requires closed : IsClosed(ℝ, realTopology, A)62  shows Countable(A) ∨63    (∃ P, Nonempty(P) ∧ Perfect(ℝ, realTopology, P) ∧ P ⊆ A)64proof65  obtain ⟨perfect, inside, countable⟩ := reals.cantorBendixson with closed66  have split : Nonempty(perfectKernel(ℝ, realTopology, A)) ∨67    ¬Nonempty(perfectKernel(ℝ, realTopology, A)) by tauto68  cases split with nonempty | empty69  . right70    exact ⟨perfectKernel(ℝ, realTopology, A), nonempty, perfect, inside⟩71  . left72    have subset : A ⊆ A ∖ perfectKernel(ℝ, realTopology, A)73      intros x hx74      apply difference.membership.backward75      refine ⟨hx, ?_⟩76      intro inKernel77      exact empty with ⟨x, inKernel⟩78    exact Countable.subset with countable, subset79