Grace/Cumulus/Topology/CantorBendixson/Derived.g17

Open in Workbench Download source

Imports

Topology.Separation

Declarations

Source

1-- Derived sets: the limit points of a set, their closure laws, and the2-- isolated points as the difference between a set and its derived set3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Topology.CantorBendixson.Derived9import Topology.Separation1011-- The derived set of A is its set of limit points.12def derivedSet (X T A : Set) : Set := limitPoints(X, T, A)1314theorem derivedSet.membership (X T A x : Set)15  shows x ∈ derivedSet(X, T, A) ↔16    x ∈ X ∧ (∀ U ∈ T, x ∈ U → Nonempty(U ∩ (A ∖ {x})))17proof18  simp [derivedSet, limitPoints.membership]1920theorem derivedSet.limit_iff (X T A x : Set)21  shows x ∈ derivedSet(X, T, A) ↔ x ∈ limitPoints(X, T, A)22proof23  simp [derivedSet]2425theorem derivedSet.subset_whole (X T A : Set)26  shows derivedSet(X, T, A) ⊆ X27proof28  unfold derivedSet29  exact limitPoints.subset at X, T, A3031theorem derivedSet.subset_closure (X T A : Set)32  requires topology : IsTopology(X, T)33  requires hA : A ⊆ X34  shows derivedSet(X, T, A) ⊆ closure(X, T, A)35proof36  unfold derivedSet37  exact limitPoints.subset_closure with topology, hA3839theorem derivedSet.subset (X T A : Set)40  requires topology : IsTopology(X, T)41  requires closed : IsClosed(X, T, A)42  shows derivedSet(X, T, A) ⊆ A43proof44  have inside := closed.left45  unfold derivedSet46  exact IsClosed.iff_limitPoints_subset.forward with topology, inside, closed4748theorem derivedSet.monotone (X T A B : Set)49  requires hAB : A ⊆ B50  shows derivedSet(X, T, A) ⊆ derivedSet(X, T, B)51proof52  unfold derivedSet53  exact limitPoints.monotone at X, T with hAB5455-- The derived set of a closed set is closed: it lies inside the set, so56-- by monotonicity its own derived set lies inside it.57theorem derivedSet.closed (X T A : Set)58  requires topology : IsTopology(X, T)59  requires closed : IsClosed(X, T, A)60  shows IsClosed(X, T, derivedSet(X, T, A))61proof62  have inside := derivedSet.subset with topology, closed63  have twice := derivedSet.monotone at X, T with inside64  have whole := derivedSet.subset_whole at X, T, A65  apply IsClosed.iff_limitPoints_subset.backward with topology, whole66  intros x hx67  have limit := derivedSet.limit_iff.backward with hx68  exact twice with x, limit6970-- In a T1 space the derived set of any subset is closed: a limit point x71-- of the derived set has, in every open U around it, a limit point y ≠ x72-- of A, and U with x removed is an open set around y that meets A.73theorem derivedSet.closed_of_t1 (X T A : Set)74  requires topology : IsTopology(X, T)75  requires t1 : IsT1Space(X, T)76  requires hA : A ⊆ X77  shows IsClosed(X, T, derivedSet(X, T, A))78proof79  have whole := derivedSet.subset_whole at X, T, A80  apply IsClosed.iff_limitPoints_subset.backward with topology, whole81  intros x hx82  have parts := limitPoints.membership.forward with hx83  apply derivedSet.membership.backward84  refine ⟨parts.left, ?_⟩85  intros U hU hxU86  obtain ⟨y, hy⟩ := parts.right with U, hU, hxU87  have inner := intersection.membership.forward with hy88  have away := difference.singleton_membership.forward with inner.right89  have yParts := derivedSet.membership.forward with away.left90  have openPoint := IsT1Space.point_complement_open with91    topology, t1, parts.left92  have openCut := IsTopology.intersection2 with topology, hU, openPoint93  have yAway : ¬y ∈ {x}94    intro same95    exact away.right with (singleton.membership.forward with same)96  have yOutside : y ∈ complement(X, {x})97    exact complement.membership.backward with ⟨yParts.left, yAway⟩98  have yCut : y ∈ U ∩ complement(X, {x})99    exact intersection.membership.backward with ⟨inner.left, yOutside⟩100  obtain ⟨z, hz⟩ := yParts.right with101    U ∩ complement(X, {x}), openCut, yCut102  have zParts := intersection.membership.forward with hz103  have zCut := intersection.membership.forward with zParts.left104  have zOutside := complement.membership.forward with zCut.right105  have zInA := difference.singleton_membership.forward with zParts.right106  have zDistinct : z ≠ x107    intro same108    apply zOutside.right109    rw same110    exact singleton.self at x111  witness z112  apply intersection.membership.backward113  refine ⟨zCut.left, ?_⟩114  exact difference.singleton_membership.backward with ⟨zInA.left, zDistinct⟩115116-- The isolated points of A: the points of A that are not limit points.117118def isolatedPoints (X T A : Set) : Set :=119  { x ∈ A | IsolatedPoint(X, T, A, x) }120121theorem derivedSet.difference (X T A : Set)122  requires topology : IsTopology(X, T)123  requires hA : A ⊆ X124  shows A ∖ derivedSet(X, T, A) = isolatedPoints(X, T, A)125proof126  ext x127  constructor128  . intro hx129    have parts := difference.membership.forward with hx130    have notLimit : ¬x ∈ limitPoints(X, T, A)131      intro limit132      exact parts.right with (derivedSet.limit_iff.backward with limit)133    have isolated := IsolatedPoint.of_not_limit with134      topology, hA, parts.left, notLimit135    exact isolatedPoints.membership.backward with ⟨parts.left, isolated⟩136  . intro hx137    have parts := isolatedPoints.membership.forward with hx138    have notLimit := IsolatedPoint.not_limit with parts.right139    apply difference.membership.backward140    refine ⟨parts.left, ?_⟩141    intro limit142    exact notLimit with (derivedSet.limit_iff.forward with limit)143144theorem derivedSet.removed_iff (X T A x : Set)145  requires topology : IsTopology(X, T)146  requires hA : A ⊆ X147  shows x ∈ A ∖ derivedSet(X, T, A) ↔ IsolatedPoint(X, T, A, x)148proof149  have split := derivedSet.difference with topology, hA150  rw split151  constructor152  . intro hx153    have parts := isolatedPoints.membership.forward with hx154    exact parts.right155  . intro isolated156    obtain ⟨hxA, U, hU, hxU, trace⟩ := isolated157    have again : IsolatedPoint(X, T, A, x) := ⟨hxA, U, hU, hxU, trace⟩158    exact isolatedPoints.membership.backward with ⟨hxA, again⟩159