Grace/Cumulus/Topology/ClosureLaws.g17

Open in Workbench Download source

Imports

Space

Declarations

Source

1-- Interior, closure, boundary, limit points, and dense sets: the laws that2-- connect them, including the duality between interior and closure under3-- complements4-- 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.ClosureLaws10import Space1112-- Interior1314theorem interiorIn.whole (X T : Set)15  requires topology : IsTopology(X, T)16  shows interiorIn(T, X) = X17proof18  exact interiorIn.of_open with (IsTopology.whole with topology)1920theorem interiorIn.empty (X T : Set)21  requires topology : IsTopology(X, T)22  shows interiorIn(T, ∅) = ∅23proof24  exact interiorIn.of_open with (IsTopology.empty with topology)2526theorem interiorIn.subset_whole (X T A : Set)27  requires topology : IsTopology(X, T)28  shows interiorIn(T, A) ⊆ X29proof30  have isOpen := interiorIn.open at X, T, A with topology31  exact IsTopology.subset with topology, isOpen3233theorem interiorIn.membership (T A x : Set)34  shows x ∈ interiorIn(T, A) ↔ ∃ U ∈ T, x ∈ U ∧ U ⊆ A35proof36  constructor37  . intro hx38    unfold interiorIn at hx39    obtain ⟨U, hU, hxU⟩ := union.membership.forward with hx40    have parts := openSubsets.membership.forward with hU41    exact ⟨U, parts.left, hxU, parts.right⟩42  . intro h43    obtain ⟨U, hU, hxU, inside⟩ := h44    have below := interiorIn.greatest with hU, inside45    exact below with x, hxU4647theorem interiorIn.subset_closure (X T A : Set)48  requires topology : IsTopology(X, T)49  requires hA : A ⊆ X50  shows interiorIn(T, A) ⊆ closure(X, T, A)51proof52  have below := interiorIn.subset at T, A53  have contains := Space.closure.contains with topology, hA54  exact Subset.transitive with below, contains5556theorem interiorIn.union2_subset (X T A B : Set)57  requires topology : IsTopology(X, T)58  shows interiorIn(T, A) ∪ interiorIn(T, B) ⊆ interiorIn(T, A ∪ B)59proof60  apply union2.subset61  . exact interiorIn.monotone with topology, (union2.subset_left at A, B)62  . exact interiorIn.monotone with topology, (union2.subset_right at A, B)6364-- Closure6566theorem closure.empty (X T : Set)67  requires topology : IsTopology(X, T)68  shows closure(X, T, ∅) = ∅69proof70  exact closure.of_closed with topology, (IsClosed.empty with topology)7172theorem closure.whole (X T : Set)73  requires topology : IsTopology(X, T)74  shows closure(X, T, X) = X75proof76  exact closure.of_closed with topology, (IsClosed.whole with topology)7778theorem closure.intersection2_subset (X T A B : Set)79  requires topology : IsTopology(X, T)80  requires hA : A ⊆ X81  requires hB : B ⊆ X82  shows closure(X, T, A ∩ B) ⊆ closure(X, T, A) ∩ closure(X, T, B)83proof84  apply intersection.greatest85  . exact closure.monotone with topology, hA, (intersection.subset_left at A, B)86  . exact closure.monotone with topology, hB, (intersection.subset_right at A, B)8788-- Duality: the closure of a complement is the complement of the interiorIn.89theorem closure.complement (X T A : Set)90  requires topology : IsTopology(X, T)91  requires hA : A ⊆ X92  shows closure(X, T, complement(X, A)) = complement(X, interiorIn(T, A))93proof94  have openInterior := interiorIn.open at X, T, A with topology95  have complementSubset := complement.subset at X, A96  apply Subset.antisymmetric97  . have closed := Open.complement_closed with topology, openInterior98    have inside := complement.antitone at X, interiorIn(T, A), A with (interiorIn.subset at T, A)99    exact closure.least with closed, inside100  . have closedClosure := closure.closed with topology, complementSubset101    have openPart := IsClosed.complement_open with closedClosure102    have contains := Space.closure.contains with topology, complementSubset103    have below := complement.antitone at X, complement(X, A), closure(X, T, complement(X, A)) with contains104    have double := complement.complement with hA105    rw double at below106    have inside := interiorIn.greatest with openPart, below107    have flipped := complement.antitone at X, complement(X, closure(X, T, complement(X, A))), interiorIn(T, A) with inside108    have closureInside := closure.subset with topology, complementSubset109    have doubleClosure := complement.complement with closureInside110    rwa doubleClosure at flipped111112theorem interiorIn.complement (X T A : Set)113  requires topology : IsTopology(X, T)114  requires hA : A ⊆ X115  shows interiorIn(T, complement(X, A)) = complement(X, closure(X, T, A))116proof117  have complementSubset := complement.subset at X, A118  have duality := closure.complement with topology, complementSubset119  have double := complement.complement with hA120  rw double at duality121  have interiorInside := interiorIn.subset_whole at X, T, complement(X, A) with topology122  have doubleInterior := complement.complement with interiorInside123  rw [duality, doubleInterior]124  rfl125126-- Boundary: the closure with the interior removed.127128def boundary (X T A : Set) : Set := closure(X, T, A) ∖ interiorIn(T, A)129130theorem boundary.membership (X T A x : Set)131  shows x ∈ boundary(X, T, A) ↔ x ∈ closure(X, T, A) ∧ ¬x ∈ interiorIn(T, A)132proof133  simp [boundary, difference.membership]134135theorem boundary.subset_closure (X T A : Set)136  shows boundary(X, T, A) ⊆ closure(X, T, A)137proof138  unfold boundary139  exact difference.subset_left140141theorem boundary.subset_whole (X T A : Set)142  requires topology : IsTopology(X, T)143  requires hA : A ⊆ X144  shows boundary(X, T, A) ⊆ X145proof146  have below := boundary.subset_closure at X, T, A147  have inside := closure.subset with topology, hA148  exact Subset.transitive with below, inside149150theorem boundary.closed (X T A : Set)151  requires topology : IsTopology(X, T)152  requires hA : A ⊆ X153  shows IsClosed(X, T, boundary(X, T, A))154proof155  have closedClosure := closure.closed with topology, hA156  have openInterior := interiorIn.open at X, T, A with topology157  have closedComplement := Open.complement_closed with topology, openInterior158  have closureInside := closure.subset with topology, hA159  have same : boundary(X, T, A) = closure(X, T, A) ∩ complement(X, interiorIn(T, A))160    ext x161    constructor162    . intro hx163      have parts := boundary.membership.forward with hx164      have hxX := closureInside with x, parts.left165      apply intersection.membership.backward166      exact ⟨parts.left, (complement.membership.backward with ⟨hxX, parts.right⟩)⟩167    . intro hx168      have parts := intersection.membership.forward with hx169      have away := complement.membership.forward with parts.right170      exact boundary.membership.backward with ⟨parts.left, away.right⟩171  rw same172  exact IsClosed.intersection2 with topology, closedClosure, closedComplement173174theorem boundary.complement (X T A : Set)175  requires topology : IsTopology(X, T)176  requires hA : A ⊆ X177  shows boundary(X, T, complement(X, A)) = boundary(X, T, A)178proof179  have closureInside := closure.subset with topology, hA180  have closureSwap := closure.complement with topology, hA181  have interiorSwap := interiorIn.complement with topology, hA182  unfold boundary183  rw [closureSwap, interiorSwap]184  ext x185  constructor186  . intro hx187    have parts := difference.membership.forward with hx188    have inComplement := complement.membership.forward with parts.left189    apply difference.membership.backward190    constructor191    . by_contra outside192      apply parts.right193      exact complement.membership.backward with ⟨inComplement.left, outside⟩194    . exact inComplement.right195  . intro hx196    have parts := difference.membership.forward with hx197    have hxX := closureInside with x, parts.left198    apply difference.membership.backward199    constructor200    . exact complement.membership.backward with ⟨hxX, parts.right⟩201    . intro away202      have awayParts := complement.membership.forward with away203      exact awayParts.right with parts.left204205theorem IsClosed.iff_boundary_subset (X T A : Set)206  requires topology : IsTopology(X, T)207  requires hA : A ⊆ X208  shows IsClosed(X, T, A) ↔ boundary(X, T, A) ⊆ A209proof210  constructor211  . intro closed212    have same := closure.of_closed with topology, closed213    have below := boundary.subset_closure at X, T, A214    rwa same at below215  . intro inside216    apply IsClosed.iff_closure.backward with topology, hA217    have interiorBelow := interiorIn.subset at T, A218    apply Subset.antisymmetric219    . intros x hx220      have split : x ∈ interiorIn(T, A) ∨ ¬x ∈ interiorIn(T, A) by tauto221      cases split with inner | outer222      . exact interiorBelow with x, inner223      . have onBoundary := boundary.membership.backward at X, T, A, x with ⟨hx, outer⟩224        exact inside with x, onBoundary225    . exact Space.closure.contains with topology, hA226227theorem Open.iff_boundary_disjoint (X T U : Set)228  requires topology : IsTopology(X, T)229  requires hU : U ⊆ X230  shows U ∈ T ↔ Disjoint(U, boundary(X, T, U))231proof232  constructor233  . intro isOpen234    have same := interiorIn.of_open with isOpen235    apply Disjoint.iff.backward236    intros x hx onBoundary237    have parts := boundary.membership.forward with onBoundary238    apply parts.right239    rwa same240  . intro disjoint241    have separated := Disjoint.iff.forward with disjoint242    have contains := Space.closure.contains with topology, hU243    apply Open.iff_interior.backward with topology244    apply Subset.antisymmetric245    . exact interiorIn.subset at T, U246    . intros x hx247      have inClosure := contains with x, hx248      by_contra outer249      apply separated with x, hx250      exact boundary.membership.backward with ⟨inClosure, outer⟩251252theorem closure.union_boundary (X T A : Set)253  requires topology : IsTopology(X, T)254  requires hA : A ⊆ X255  shows closure(X, T, A) = A ∪ boundary(X, T, A)256proof257  have contains := Space.closure.contains with topology, hA258  have interiorBelow := interiorIn.subset at T, A259  apply Subset.antisymmetric260  . intros x hx261    apply union2.membership.backward262    have split : x ∈ interiorIn(T, A) ∨ ¬x ∈ interiorIn(T, A) by tauto263    cases split with inner | outer264    . left265      exact interiorBelow with x, inner266    . right267      exact boundary.membership.backward with ⟨hx, outer⟩268  . apply union2.subset269    . exact contains270    . exact boundary.subset_closure at X, T, A271272theorem interiorIn.difference_boundary (X T A : Set)273  requires topology : IsTopology(X, T)274  requires hA : A ⊆ X275  shows interiorIn(T, A) = A ∖ boundary(X, T, A)276proof277  have contains := Space.closure.contains with topology, hA278  have interiorBelow := interiorIn.subset at T, A279  ext x280  constructor281  . intro hx282    apply difference.membership.backward283    constructor284    . exact interiorBelow with x, hx285    . intro onBoundary286      have parts := boundary.membership.forward with onBoundary287      exact parts.right with hx288  . intro hx289    have parts := difference.membership.forward with hx290    have inClosure := contains with x, parts.left291    by_contra outer292    apply parts.right293    exact boundary.membership.backward with ⟨inClosure, outer⟩294295theorem boundary.whole (X T : Set)296  requires topology : IsTopology(X, T)297  shows boundary(X, T, X) = ∅298proof299  have closureWhole := closure.whole with topology300  have interiorWhole := interiorIn.whole with topology301  simp [boundary]302  exact difference.self at X303304theorem boundary.empty (X T : Set)305  requires topology : IsTopology(X, T)306  shows boundary(X, T, ∅) = ∅307proof308  have closureEmpty := closure.empty with topology309  have interiorEmpty := interiorIn.empty with topology310  simp [boundary]311  exact difference.self at ∅312313-- A set that is both open and closed has no boundary.314theorem boundary.empty_of_clopen (X T U : Set)315  requires topology : IsTopology(X, T)316  requires isOpen : U ∈ T317  requires closed : IsClosed(X, T, U)318  shows boundary(X, T, U) = ∅319proof320  have closureSame := closure.of_closed with topology, closed321  have interiorSame := interiorIn.of_open with isOpen322  simp [boundary]323  exact difference.self at U324325theorem boundary.boundary_subset (X T A : Set)326  requires topology : IsTopology(X, T)327  requires hA : A ⊆ X328  shows boundary(X, T, boundary(X, T, A)) ⊆ boundary(X, T, A)329proof330  have closed := boundary.closed with topology, hA331  have same := closure.of_closed with topology, closed332  have below := boundary.subset_closure at X, T, boundary(X, T, A)333  rwa same at below334335-- Limit points: every open set around x meets A away from x.336337def limitPoints (X T A : Set) : Set :=338  { x ∈ X | ∀ U ∈ T, x ∈ U → Nonempty(U ∩ (A ∖ {x})) }339340theorem limitPoints.subset (X T A : Set)341  shows limitPoints(X, T, A) ⊆ X342proof343  intros x hx344  have parts := limitPoints.membership.forward with hx345  exact parts.left346347theorem limitPoints.subset_closure (X T A : Set)348  requires topology : IsTopology(X, T)349  requires hA : A ⊆ X350  shows limitPoints(X, T, A) ⊆ closure(X, T, A)351proof352  intros x hx353  have parts := limitPoints.membership.forward with hx354  apply closure.membership.backward with topology, hA355  refine ⟨parts.left, ?_⟩356  intros U hU hxU357  obtain ⟨a, ha⟩ := parts.right with U, hU, hxU358  have inner := intersection.membership.forward with ha359  have away := difference.singleton_membership.forward with inner.right360  witness a361  exact intersection.membership.backward with ⟨inner.left, away.left⟩362363theorem closure.union_limitPoints (X T A : Set)364  requires topology : IsTopology(X, T)365  requires hA : A ⊆ X366  shows closure(X, T, A) = A ∪ limitPoints(X, T, A)367proof368  apply Subset.antisymmetric369  . intros x hx370    have parts := closure.membership.forward with topology, hA, hx371    apply union2.membership.backward372    have split : x ∈ A ∨ ¬x ∈ A by tauto373    cases split with inA | outside374    . left375      exact inA376    . right377      apply limitPoints.membership.backward378      refine ⟨parts.left, ?_⟩379      intros U hU hxU380      obtain ⟨a, ha⟩ := parts.right with U, hU, hxU381      have inner := intersection.membership.forward with ha382      have distinct : a ≠ x383        intro same384        apply outside385        rw ← same386        exact inner.right387      witness a388      apply intersection.membership.backward389      refine ⟨inner.left, ?_⟩390      exact difference.singleton_membership.backward with ⟨inner.right, distinct⟩391  . apply union2.subset392    . exact Space.closure.contains with topology, hA393    . exact limitPoints.subset_closure with topology, hA394395theorem IsClosed.iff_limitPoints_subset (X T A : Set)396  requires topology : IsTopology(X, T)397  requires hA : A ⊆ X398  shows IsClosed(X, T, A) ↔ limitPoints(X, T, A) ⊆ A399proof400  constructor401  . intro closed402    have same := closure.of_closed with topology, closed403    have below := limitPoints.subset_closure with topology, hA404    rwa same at below405  . intro inside406    apply IsClosed.iff_closure.backward with topology, hA407    have split := closure.union_limitPoints with topology, hA408    rw split409    apply Subset.antisymmetric410    . exact union2.subset with (Subset.reflexive at A), inside411    . exact union2.subset_left at A, limitPoints(X, T, A)412413theorem limitPoints.monotone (X T A B : Set)414  requires hAB : A ⊆ B415  shows limitPoints(X, T, A) ⊆ limitPoints(X, T, B)416proof417  intros x hx418  have parts := limitPoints.membership.forward with hx419  apply limitPoints.membership.backward420  refine ⟨parts.left, ?_⟩421  intros U hU hxU422  obtain ⟨a, ha⟩ := parts.right with U, hU, hxU423  have inner := intersection.membership.forward with ha424  have away := difference.singleton_membership.forward with inner.right425  witness a426  apply intersection.membership.backward427  refine ⟨inner.left, ?_⟩428  exact difference.singleton_membership.backward with ⟨(hAB with a, away.left), away.right⟩429430-- Isolated points: some open set around x meets A only in x.431432predicate IsolatedPoint (X T A x : Set) :=433  x ∈ A ∧ ∃ U ∈ T, x ∈ U ∧ U ∩ A = {x}434435theorem IsolatedPoint.not_limit (X T A x : Set)436  requires isolated : IsolatedPoint(X, T, A, x)437  shows ¬x ∈ limitPoints(X, T, A)438proof439  obtain ⟨hxA, U, hU, hxU, trace⟩ := isolated440  intro limit441  have parts := limitPoints.membership.forward with limit442  obtain ⟨a, ha⟩ := parts.right with U, hU, hxU443  have inner := intersection.membership.forward with ha444  have away := difference.singleton_membership.forward with inner.right445  have inTrace : a ∈ U ∩ A := intersection.membership.backward with ⟨inner.left, away.left⟩446  rw trace at inTrace447  have same := singleton.membership.forward with inTrace448  exact away.right with same449450theorem IsolatedPoint.of_not_limit (X T A x : Set)451  requires topology : IsTopology(X, T)452  requires hA : A ⊆ X453  requires hxA : x ∈ A454  requires notLimit : ¬x ∈ limitPoints(X, T, A)455  shows IsolatedPoint(X, T, A, x)456proof457  have hxX := hA with x, hxA458  refine ⟨hxA, ?_⟩459  by_contra none460  apply notLimit461  apply limitPoints.membership.backward462  refine ⟨hxX, ?_⟩463  intros U hU hxU464  by_contra empty465  apply none466  refine ⟨U, hU, hxU, ?_⟩467  ext y468  constructor469  . intro hy470    have parts := intersection.membership.forward with hy471    apply singleton.membership.backward472    by_contra distinct473    apply empty474    witness y475    apply intersection.membership.backward476    refine ⟨parts.left, ?_⟩477    exact difference.singleton_membership.backward with ⟨parts.right, distinct⟩478  . intro hy479    have same := singleton.membership.forward with hy480    rw same481    exact intersection.membership.backward with ⟨hxU, hxA⟩482483theorem IsolatedPoint.iff (X T A x : Set)484  requires topology : IsTopology(X, T)485  requires hA : A ⊆ X486  requires hxA : x ∈ A487  shows IsolatedPoint(X, T, A, x) ↔ ¬x ∈ limitPoints(X, T, A)488proof489  constructor490  . intro isolated491    exact IsolatedPoint.not_limit with isolated492  . intro notLimit493    exact IsolatedPoint.of_not_limit with topology, hA, hxA, notLimit494495-- Dense sets496497theorem IsDense.whole (X T : Set)498  requires topology : IsTopology(X, T)499  shows IsDense(X, T, X)500proof501  exact closure.whole with topology502503theorem IsDense.iff_meets_open (X T A : Set)504  requires topology : IsTopology(X, T)505  requires hA : A ⊆ X506  shows IsDense(X, T, A) ↔ ∀ U ∈ T, Nonempty(U) → Nonempty(U ∩ A)507proof508  constructor509  . intros dense U hU inhabited510    have equal : closure(X, T, A) = X := dense511    obtain ⟨x, hx⟩ := inhabited512    have inside := IsTopology.subset with topology, hU513    have hxX := inside with x, hx514    have inClosure : x ∈ closure(X, T, A)515      rw equal516      exact hxX517    have parts := closure.membership.forward with topology, hA, inClosure518    exact parts.right with U, hU, hx519  . intro meets520    have inside := closure.subset with topology, hA521    have equal : closure(X, T, A) = X522      apply Subset.antisymmetric523      . exact inside524      . intros x hx525        apply closure.membership.backward with topology, hA526        refine ⟨hx, ?_⟩527        intros U hU hxU528        have inhabited : Nonempty(U) := ⟨x, hxU⟩529        exact meets with U, hU, inhabited530    exact equal531532theorem IsDense.of_subset (X T A B : Set)533  requires topology : IsTopology(X, T)534  requires hB : B ⊆ X535  requires hAB : A ⊆ B536  requires dense : IsDense(X, T, A)537  shows IsDense(X, T, B)538proof539  have equal : closure(X, T, A) = X := dense540  have below := closure.monotone with topology, hB, hAB541  have inside := closure.subset with topology, hB542  rw equal at below543  exact Subset.antisymmetric with inside, below544545theorem IsDense.meets (X T A U : Set)546  requires topology : IsTopology(X, T)547  requires hA : A ⊆ X548  requires dense : IsDense(X, T, A)549  requires hU : U ∈ T550  requires inhabited : Nonempty(U)551  shows Nonempty(U ∩ A)552proof553  have meets := IsDense.iff_meets_open.forward with topology, hA, dense554  exact meets with U, hU, inhabited555556theorem IsDense.interior_complement (X T A : Set)557  requires topology : IsTopology(X, T)558  requires hA : A ⊆ X559  shows IsDense(X, T, A) ↔ interiorIn(T, complement(X, A)) = ∅560proof561  have swap := interiorIn.complement with topology, hA562  have inside := closure.subset with topology, hA563  rw swap564  constructor565  . intro dense566    have equal : closure(X, T, A) = X := dense567    rw equal568    exact complement.self at X569  . intro empty570    unfold complement at empty571    have below := difference.eq_empty_iff.forward with empty572    exact Subset.antisymmetric with inside, below573