Grace/Cumulus/Topology/Structure.g17

Open in Workbench Download source

Imports

Maps · Basis · Connected

Declarations

Source

1-- Bundled topological spaces: a space as one structure of its carrier and2-- its open sets, the open and closed sets, neighborhoods, interior,3-- closure, density, and convergent sequences under their standard names,4-- the closure instances, and the topology rewrite set5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.Topology.Structure11import Maps12import Basis13import Connected1415-- A topological space is a structure of its carrier and its family of open16-- sets, built by TopologicalSpace.mk(A, T) and read back by the projections17-- X.carrier and X.opens. TopologicalSpace(X) says that X is such a18-- structure whose open sets are subsets of the carrier containing the19-- carrier and closed under arbitrary unions and binary intersections; the20-- empty set is the union of the empty family. IsTopology(A, T) remains the21-- form over separate pieces, bridged below.22structure TopologicalSpace23  | carrier : Set24  | opens : Set25  where26    opens_subsets : opens ⊆ 𝒫(carrier)27    carrier_open : carrier ∈ opens28    union_open : ∀ S, S ⊆ opens → ⋃(S) ∈ opens29    inter_open : ∀ U V ∈ opens, U ∩ V ∈ opens3031-- The projection laws of a constructed space as one rewrite set.32tactic topology_projections := simp [TopologicalSpace.mk.carrier, TopologicalSpace.mk.opens]3334-- Bridges between the structure and the form over separate pieces. The35-- bundled-to-unbundled direction is an instance, so `with *` reads the36-- topology off a space hypothesis.37instance TopologicalSpace.parts (X : Set)38  requires space : TopologicalSpace(X)39  shows IsTopology(X.carrier, X.opens)40proof41  obtain ⟨shape, subsets, whole, unions, intersections⟩ := space42  unfold IsTopology43  exact ⟨subsets, whole, unions, intersections⟩4445theorem TopologicalSpace.of_parts (A T : Set)46  requires topology : IsTopology(A, T)47  shows TopologicalSpace(TopologicalSpace.mk(A, T))48proof49  obtain ⟨subsets, whole, unions, intersections⟩ := topology50  apply TopologicalSpace.intro51  . exact subsets52  . exact whole53  . exact unions54  . exact intersections5556theorem TopologicalSpace.of_projections (X : Set)57  requires shape : TopologicalSpace.Data(X)58  requires topology : IsTopology(X.carrier, X.opens)59  shows TopologicalSpace(X)60proof61  obtain ⟨subsets, whole, unions, intersections⟩ := topology62  unfold TopologicalSpace63  exact ⟨shape, subsets, whole, unions, intersections⟩6465-- A space is the constructor applied to its projections.66theorem TopologicalSpace.eta_of_space (X : Set)67  requires space : TopologicalSpace(X)68  shows X = TopologicalSpace.mk(X.carrier, X.opens)69proof70  obtain ⟨shape, rest⟩ := space71  exact TopologicalSpace.eta with shape7273-- Under a hypothesis TopologicalSpace(X): Open(X, U) says U is open, that74-- is, U ∈ X.opens; Closed(X, C) that C is a subset of the carrier whose75-- complement is open; Neighborhood(X, N, x) that N contains an open set76-- around x; Dense(X, A) that A meets every nonempty open set; Compact(X, A)77-- that every open cover of A has a finite subcover; ConnectedSubset(X, A)78-- that A has no separation by open sets; and Converges(X, u, x), written79-- u ⇝ x, that the sequence u in X is eventually inside every open set80-- around x. IsClosed(A, T, C), IsDense(A, T, C), IsCompact(A, T, C), and81-- IsConnectedSubset(A, T, C) remain the forms over separate pieces.82section Definitions83variable (X : Set)84hypothesis space : TopologicalSpace(X)8586predicate Open (U : Set) := U ∈ X.opens87predicate Closed (C : Set) := IsClosed(X.carrier, X.opens, C)88predicate Neighborhood (N x : Set) :=89  N ⊆ X.carrier ∧ (∃ U ∈ X.opens, x ∈ U ∧ U ⊆ N)90predicate Dense (A : Set) := IsDense(X.carrier, X.opens, A)91predicate Compact (A : Set) := IsCompact(X.carrier, X.opens, A)92predicate ConnectedSubset (A : Set) := IsConnectedSubset(X.carrier, X.opens, A)93predicate Converges (u x : Set) :=94  (u : ℕ → X.carrier) ∧ x ∈ X.carrier ∧95  (∀ U ∈ X.opens, x ∈ U →96    ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → u(n) ∈ U)9798end Definitions99100-- The properties of the space itself: Compact(X) says the carrier is a101-- compact subset, the one-place form beside Compact(X, A) resolved by its102-- arity, Hausdorff(X) that distinct points have disjoint open103-- neighborhoods, T1Space(X) that each point is closed, and Connected(X)104-- that the carrier is not the union of two disjoint nonempty open sets.105-- IsCompact(A, T, A), IsHausdorff(A, T), IsT1Space(A, T), and IsConnected(A, T)106-- remain the forms over separate pieces.107predicate Compact (X : Set) :=108  IsCompact(TopologicalSpace.carrier(X), TopologicalSpace.opens(X),109    TopologicalSpace.carrier(X))110predicate Hausdorff (X : Set) :=111  IsHausdorff(TopologicalSpace.carrier(X), TopologicalSpace.opens(X))112predicate T1Space (X : Set) :=113  IsT1Space(TopologicalSpace.carrier(X), TopologicalSpace.opens(X))114predicate Connected (X : Set) :=115  IsConnected(TopologicalSpace.carrier(X), TopologicalSpace.opens(X))116117-- A sequence converging to a point is written u ⇝ x wherever a hypothesis118-- in scope supplies the space. Under the same hypothesis a binder (x : X)119-- is a set variable with x ∈ X.carrier, and x ∈ X, U ⊆ X, and ∀ x ∈ X120-- are read at the carrier.121notation infix 50 "⇝" => Converges(X, _, _) via hypothesis TopologicalSpace(X) for X.carrier122123-- The interior of A is the largest open set inside A, its closure the124-- smallest closed set around it, and its boundary the closure minus the125-- interior. interiorIn(T, A), closure(A, T, S), and boundary(A, T, S)126-- remain the forms over separate pieces.127def interior (X A : Set) : Set := interiorIn(TopologicalSpace.opens(X), A)128def closure (X A : Set) : Set :=129  closure(TopologicalSpace.carrier(X), TopologicalSpace.opens(X), A)130def boundary (X A : Set) : Set :=131  boundary(TopologicalSpace.carrier(X), TopologicalSpace.opens(X), A)132133theorem interior.parts (X A : Set)134  shows interior(X, A) = interiorIn(TopologicalSpace.opens(X), A)135proof136  simp [interior]137138theorem closure.parts (X A : Set)139  shows closure(X, A) =140    closure(TopologicalSpace.carrier(X), TopologicalSpace.opens(X), A)141proof142  simp [closure]143144theorem boundary.parts (X A : Set)145  shows boundary(X, A) =146    boundary(TopologicalSpace.carrier(X), TopologicalSpace.opens(X), A)147proof148  simp [boundary]149150section OpenLaws151variable (X : Set)152hypothesis space : TopologicalSpace(X)153154-- Open(X, U) and U ∈ X.opens are the same fact; the forward direction is155-- an instance, so an engine requirement U ∈ X.opens is read off Open(X, U).156instance Open.mem (U : Set)157  requires open : Open(X, U)158  shows U ∈ X.opens159proof160  unfold Open at open161  exact open162163theorem Open.of_mem (U : Set)164  requires member : U ∈ X.opens165  shows Open(X, U)166proof167  unfold Open168  exact member169170theorem Open.subset (U : Set)171  requires open : Open(X, U)172  shows U ⊆ X173proof174  have member := Open.mem with open175  exact IsTopology.subset with *176177theorem Open.point (U x : Set)178  requires open : Open(X, U)179  requires hx : x ∈ U180  shows x ∈ X181proof182  have inside := Open.subset with open183  exact inside with x, hx184185-- Closure: the carrier, the empty set, binary intersections, and unions of186-- open sets are open. These are instances, so openness of a compound set is187-- synthesized.188instance Open.carrier189  shows Open(X, X.carrier)190proof191  have parts := TopologicalSpace.parts with space192  unfold Open193  exact IsTopology.whole with *194195instance Open.empty_set196  shows Open(X, ∅)197proof198  have parts := TopologicalSpace.parts with space199  unfold Open200  exact IsTopology.empty with *201202instance Open.inter (U V : Set)203  requires openU : Open(X, U)204  requires openV : Open(X, V)205  shows Open(X, U ∩ V)206proof207  have parts := TopologicalSpace.parts with space208  have memberU := Open.mem with openU209  have memberV := Open.mem with openV210  unfold Open211  exact IsTopology.intersection2 with *212213instance Open.union (U V : Set)214  requires openU : Open(X, U)215  requires openV : Open(X, V)216  shows Open(X, U ∪ V)217proof218  have parts := TopologicalSpace.parts with space219  have memberU := Open.mem with openU220  have memberV := Open.mem with openV221  unfold Open222  exact IsTopology.union2 with *223224theorem Open.family_union (S : Set)225  requires opens : ∀ U ∈ S, Open(X, U)226  shows Open(X, ⋃(S))227proof228  have parts := TopologicalSpace.parts with space229  have inside : S ⊆ X.opens230    intros U hU231    exact Open.mem with (opens with U, hU)232  unfold Open233  exact IsTopology.union with *234235theorem Open.finite_inter (S : Set)236  requires finite : Finite(S)237  requires nonempty : Nonempty(S)238  requires opens : ∀ U ∈ S, Open(X, U)239  shows Open(X, ⋂(S))240proof241  have parts := TopologicalSpace.parts with space242  have inside : S ⊆ X.opens243    intros U hU244    exact Open.mem with (opens with U, hU)245  unfold Open246  exact IsTopology.finite_intersection with *247248-- Closed sets.249instance Closed.parts (C : Set)250  requires closed : Closed(X, C)251  shows IsClosed(X.carrier, X.opens, C)252proof253  unfold Closed at closed254  exact closed255256theorem Closed.of_parts (C : Set)257  requires closed : IsClosed(X.carrier, X.opens, C)258  shows Closed(X, C)259proof260  unfold Closed261  exact closed262263theorem Closed.subset (C : Set)264  requires closed : Closed(X, C)265  shows C ⊆ X266proof267  have parts := Closed.parts with closed268  exact parts.left269270theorem Closed.compl_open (C : Set)271  requires closed : Closed(X, C)272  shows Open(X, complement(X.carrier, C))273proof274  have parts := Closed.parts with closed275  unfold Open276  exact parts.right277278theorem Open.compl_closed (U : Set)279  requires open : Open(X, U)280  shows Closed(X, complement(X.carrier, U))281proof282  have member := Open.mem with open283  unfold Closed284  exact Space.Open.complement_closed with *285286instance Closed.carrier287  shows Closed(X, X.carrier)288proof289  unfold Closed290  exact Space.IsClosed.whole with *291292instance Closed.empty_set293  shows Closed(X, ∅)294proof295  unfold Closed296  exact Space.IsClosed.empty with *297298instance Closed.union (C D : Set)299  requires closedC : Closed(X, C)300  requires closedD : Closed(X, D)301  shows Closed(X, C ∪ D)302proof303  have partsC := Closed.parts with closedC304  have partsD := Closed.parts with closedD305  unfold Closed306  exact IsClosed.union2 with *307308instance Closed.inter (C D : Set)309  requires closedC : Closed(X, C)310  requires closedD : Closed(X, D)311  shows Closed(X, C ∩ D)312proof313  have partsC := Closed.parts with closedC314  have partsD := Closed.parts with closedD315  unfold Closed316  exact IsClosed.intersection2 with *317318theorem Closed.family_inter (S : Set)319  requires nonempty : Nonempty(S)320  requires closed : ∀ C ∈ S, Closed(X, C)321  shows Closed(X, ⋂(S))322proof323  have pieces : ∀ C ∈ S, IsClosed(X.carrier, X.opens, C)324    intros C hC325    exact Closed.parts with (closed with C, hC)326  unfold Closed327  exact IsClosed.family_intersection with *328329-- The textbook law: a set is open exactly when it is a neighborhood of each330-- of its points.331theorem Neighborhood.of_open (U x : Set)332  requires open : Open(X, U)333  requires hx : x ∈ U334  shows Neighborhood(X, U, x)335proof336  have member := Open.mem with open337  have inside := Open.subset with open338  unfold Neighborhood339  exact ⟨inside, U, member, hx, (Subset.reflexive at U)⟩340341theorem Neighborhood.point (N x : Set)342  requires neighborhood : Neighborhood(X, N, x)343  shows x ∈ N344proof345  obtain ⟨inside, U, hU, hxU, hUN⟩ := neighborhood346  exact hUN with x, hxU347348theorem Neighborhood.superset (N M x : Set)349  requires neighborhood : Neighborhood(X, N, x)350  requires hNM : N ⊆ M351  requires hM : M ⊆ X352  shows Neighborhood(X, M, x)353proof354  obtain ⟨inside, U, hU, hxU, hUN⟩ := neighborhood355  unfold Neighborhood356  exact ⟨hM, U, hU, hxU, (Subset.transitive with hUN, hNM)⟩357358theorem Neighborhood.inter (N M x : Set)359  requires first : Neighborhood(X, N, x)360  requires second : Neighborhood(X, M, x)361  shows Neighborhood(X, N ∩ M, x)362proof363  have parts := TopologicalSpace.parts with space364  obtain ⟨insideN, U, hU, hxU, hUN⟩ := first365  obtain ⟨insideM, V, hV, hxV, hVM⟩ := second366  have both : U ∩ V ∈ X.opens := IsTopology.intersection2 with *367  have point : x ∈ U ∩ V368    exact intersection.membership.backward with ⟨hxU, hxV⟩369  have below := intersection.subset_left at N, M370  have inside : N ∩ M ⊆ X.carrier := Subset.transitive with below, insideN371  unfold Neighborhood372  refine ⟨inside, U ∩ V, both, point, ?_⟩373  exact intersection.monotone with hUN, hVM374375theorem Open.iff_neighborhoods (U : Set)376  requires hU : U ⊆ X377  shows Open(X, U) ↔ ∀ x ∈ U, Neighborhood(X, U, x)378proof379  have parts := TopologicalSpace.parts with space380  constructor381  . intros open x hx382    exact Neighborhood.of_open with *383  . intro around384    have cover : U = ⋃(openSubsets(X.opens, U))385      apply Subset.antisymmetric386      . intros x hx387        obtain ⟨inside, V, hV, hxV, hVU⟩ := around with x, hx388        have member : V ∈ openSubsets(X.opens, U)389          exact openSubsets.membership.backward with ⟨hV, hVU⟩390        exact union.contains with member, hxV391      . apply union.subset392        intros V hV393        have pieces := openSubsets.membership.forward with hV394        exact pieces.right395    have inside : openSubsets(X.opens, U) ⊆ X.opens396      intros V hV397      have pieces := openSubsets.membership.forward with hV398      exact pieces.left399    rw cover400    exact Open.of_mem with (IsTopology.union with *)401402end OpenLaws403404section InteriorClosureLaws405variable (X : Set)406hypothesis space : TopologicalSpace(X)407408-- The interior laws, under their standard names.409instance interior_open (A : Set)410  shows Open(X, interior(X, A))411proof412  have parts := TopologicalSpace.parts with space413  unfold Open414  rw interior.parts415  exact interiorIn.open with *416417theorem interior_subset (A : Set)418  shows interior(X, A) ⊆ A419proof420  rw interior.parts421  exact interiorIn.subset at X.opens, A422423theorem interior_maximal (A U : Set)424  requires open : Open(X, U)425  requires inside : U ⊆ A426  shows U ⊆ interior(X, A)427proof428  have member := Open.mem with open429  rw interior.parts430  exact interiorIn.greatest with *431432theorem interior_eq_of_open (U : Set)433  requires open : Open(X, U)434  shows interior(X, U) = U435proof436  have member := Open.mem with open437  rw interior.parts438  exact interiorIn.of_open with *439440theorem interior_eq_iff_open (U : Set)441  shows interior(X, U) = U ↔ Open(X, U)442proof443  constructor444  . intro equal445    rw ← equal446    exact interior_open with *447  . intro open448    exact interior_eq_of_open with *449450theorem mem_interior (A x : Set)451  shows x ∈ interior(X, A) ↔ ∃ U, Open(X, U) ∧ x ∈ U ∧ U ⊆ A452proof453  rw interior.parts454  have characterization := interiorIn.membership at X.opens, A, x455  constructor456  . intro hx457    obtain ⟨U, hU, hxU, hUA⟩ := characterization.forward with hx458    exact ⟨U, (Open.of_mem with hU), hxU, hUA⟩459  . intro inside460    obtain ⟨U, open, hxU, hUA⟩ := inside461    have member := Open.mem with open462    exact characterization.backward with ⟨U, member, hxU, hUA⟩463464theorem interior_mono (A B : Set)465  requires hAB : A ⊆ B466  shows interior(X, A) ⊆ interior(X, B)467proof468  have parts := TopologicalSpace.parts with space469  rw [interior.parts, interior.parts]470  exact interiorIn.monotone with *471472theorem interior_interior (A : Set)473  shows interior(X, interior(X, A)) = interior(X, A)474proof475  have parts := TopologicalSpace.parts with space476  rw [interior.parts, interior.parts]477  exact interiorIn.idempotent with *478479theorem interior_inter (A B : Set)480  shows interior(X, A ∩ B) = interior(X, A) ∩ interior(X, B)481proof482  have parts := TopologicalSpace.parts with space483  rw [interior.parts, interior.parts, interior.parts]484  exact interiorIn.intersection2 with *485486theorem interior_whole487  shows interior(X, X.carrier) = X.carrier488proof489  have parts := TopologicalSpace.parts with space490  rw interior.parts491  exact interiorIn.whole with *492493theorem interior_empty494  shows interior(X, ∅) = ∅495proof496  have parts := TopologicalSpace.parts with space497  rw interior.parts498  exact interiorIn.empty with *499500-- The closure laws.501instance closure_closed (A : Set)502  requires hA : A ⊆ X503  shows Closed(X, closure(X, A))504proof505  have parts := TopologicalSpace.parts with space506  unfold Closed507  rw closure.parts508  exact Space.closure.closed with *509510theorem subset_closure (A : Set)511  requires hA : A ⊆ X512  shows A ⊆ closure(X, A)513proof514  have parts := TopologicalSpace.parts with space515  rw closure.parts516  exact Space.closure.contains with *517518theorem closure_minimal (A C : Set)519  requires closed : Closed(X, C)520  requires hAC : A ⊆ C521  shows closure(X, A) ⊆ C522proof523  have parts := TopologicalSpace.parts with space524  have pieces := Closed.parts with closed525  rw closure.parts526  exact closure.least with *527528theorem closure_subset (A : Set)529  requires hA : A ⊆ X530  shows closure(X, A) ⊆ X531proof532  have parts := TopologicalSpace.parts with space533  rw closure.parts534  exact Space.closure.subset with *535536theorem closure_eq_of_closed (C : Set)537  requires closed : Closed(X, C)538  shows closure(X, C) = C539proof540  have parts := TopologicalSpace.parts with space541  have pieces := Closed.parts with closed542  rw closure.parts543  exact closure.of_closed with *544545theorem closure_eq_iff_closed (C : Set)546  requires hC : C ⊆ X547  shows closure(X, C) = C ↔ Closed(X, C)548proof549  constructor550  . intro equal551    rw ← equal552    exact closure_closed with *553  . intro closed554    exact closure_eq_of_closed with *555556theorem closure_mono (A B : Set)557  requires hB : B ⊆ X558  requires hAB : A ⊆ B559  shows closure(X, A) ⊆ closure(X, B)560proof561  have parts := TopologicalSpace.parts with space562  rw [closure.parts, closure.parts]563  exact closure.monotone with *564565theorem closure_closure (A : Set)566  requires hA : A ⊆ X567  shows closure(X, closure(X, A)) = closure(X, A)568proof569  have parts := TopologicalSpace.parts with space570  rw [closure.parts, closure.parts]571  exact closure.idempotent with *572573theorem closure_union (A B : Set)574  requires hA : A ⊆ X575  requires hB : B ⊆ X576  shows closure(X, A ∪ B) = closure(X, A) ∪ closure(X, B)577proof578  have parts := TopologicalSpace.parts with space579  rw [closure.parts, closure.parts, closure.parts]580  exact closure.union2 with *581582theorem closure_whole583  shows closure(X, X.carrier) = X.carrier584proof585  have parts := TopologicalSpace.parts with space586  rw closure.parts587  exact closure.whole with *588589theorem closure_empty590  shows closure(X, ∅) = ∅591proof592  have parts := TopologicalSpace.parts with space593  rw closure.parts594  exact closure.empty with *595596-- A point lies in the closure of A exactly when every open set around it597-- meets A.598theorem mem_closure (A x : Set)599  requires hA : A ⊆ X600  shows x ∈ closure(X, A) ↔601    x ∈ X ∧ (∀ U, Open(X, U) → x ∈ U → Nonempty(U ∩ A))602proof603  have parts := TopologicalSpace.parts with space604  rw closure.parts605  have criterion := closure.membership at X.carrier, X.opens, A, x with parts, hA606  constructor607  . intro hx608    obtain ⟨inX, meets⟩ := criterion.forward with hx609    refine ⟨inX, ?_⟩610    intros U open hxU611    have member := Open.mem with open612    exact meets with U, member, hxU613  . intro meets614    obtain ⟨inX, touches⟩ := meets615    apply criterion.backward616    refine ⟨inX, ?_⟩617    intros U hU hxU618    exact touches with U, (Open.of_mem with hU), hxU619620theorem interior_subset_closure (A : Set)621  requires hA : A ⊆ X622  shows interior(X, A) ⊆ closure(X, A)623proof624  have parts := TopologicalSpace.parts with space625  rw [interior.parts, closure.parts]626  exact interiorIn.subset_closure with *627628theorem closure_complement (A : Set)629  requires hA : A ⊆ X630  shows closure(X, complement(X.carrier, A)) =631    complement(X.carrier, interior(X, A))632proof633  have parts := TopologicalSpace.parts with space634  rw [interior.parts, closure.parts]635  exact closure.complement with *636637theorem interior_complement (A : Set)638  requires hA : A ⊆ X639  shows interior(X, complement(X.carrier, A)) =640    complement(X.carrier, closure(X, A))641proof642  have parts := TopologicalSpace.parts with space643  rw [interior.parts, closure.parts]644  exact interiorIn.complement with *645646-- The boundary.647theorem mem_boundary (A x : Set)648  shows x ∈ boundary(X, A) ↔ x ∈ closure(X, A) ∧ ¬x ∈ interior(X, A)649proof650  rw [boundary.parts, closure.parts, interior.parts]651  exact boundary.membership at X.carrier, X.opens, A, x652653instance boundary_closed (A : Set)654  requires hA : A ⊆ X655  shows Closed(X, boundary(X, A))656proof657  have parts := TopologicalSpace.parts with space658  unfold Closed659  rw boundary.parts660  exact ClosureLaws.boundary.closed with *661662-- Dense sets.663instance Dense.parts (A : Set)664  requires dense : Dense(X, A)665  shows IsDense(X.carrier, X.opens, A)666proof667  unfold Dense at dense668  exact dense669670theorem Dense.of_parts (A : Set)671  requires dense : IsDense(X.carrier, X.opens, A)672  shows Dense(X, A)673proof674  unfold Dense675  exact dense676677theorem Dense.closure (A : Set)678  requires dense : Dense(X, A)679  shows closure(X, A) = X.carrier680proof681  have parts := Dense.parts with dense682  rw closure.parts683  unfold IsDense at parts684  exact parts685686theorem Dense.carrier687  shows Dense(X, X.carrier)688proof689  have parts := TopologicalSpace.parts with space690  unfold Dense691  exact ClosureLaws.IsDense.whole with *692693theorem Dense.iff_meets (A : Set)694  requires hA : A ⊆ X695  shows Dense(X, A) ↔ ∀ U, Open(X, U) → Nonempty(U) → Nonempty(U ∩ A)696proof697  have parts := TopologicalSpace.parts with space698  have characterization := ClosureLaws.IsDense.iff_meets_open with *699  constructor700  . intros dense U open inhabited701    have pieces := Dense.parts with dense702    have member := Open.mem with open703    exact characterization.forward with pieces, U, member, inhabited704  . intro meets705    have pieces : ∀ U ∈ X.opens, Nonempty(U) → Nonempty(U ∩ A)706      intros U hU inhabited707      exact meets with U, (Open.of_mem with hU), inhabited708    exact Dense.of_parts with (characterization.backward with pieces)709710end InteriorClosureLaws711712-- The topology rewrite set: the idempotent and distributive laws of713-- interior and closure, their values on the carrier and the empty set, and714-- their values on open and closed sets.715tactic topology_simp := simp [interior_interior, closure_closure, interior_inter, closure_union, interior_whole, interior_empty, closure_whole, closure_empty, interior_eq_of_open, closure_eq_of_closed]716717section ConvergenceLaws718variable (X : Set)719hypothesis space : TopologicalSpace(X)720721theorem Converges.sequence (u x : Set)722  requires converges : u ⇝ x723  shows u : ℕ → X.carrier724proof725  obtain ⟨sequence, point, eventually⟩ := converges726  exact sequence727728theorem Converges.limit_mem (u x : Set)729  requires converges : u ⇝ x730  shows x ∈ X731proof732  obtain ⟨sequence, point, eventually⟩ := converges733  exact point734735theorem Converges.eventually (u x U : Set)736  requires converges : u ⇝ x737  requires open : Open(X, U)738  requires hx : x ∈ U739  shows ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → u(n) ∈ U740proof741  obtain ⟨sequence, point, eventually⟩ := converges742  have member := Open.mem with open743  exact eventually with U, member, hx744745theorem Converges.of_eventually (u x : Set)746  requires sequence : u : ℕ → X.carrier747  requires point : x ∈ X748  requires eventually : ∀ U, Open(X, U) → x ∈ U →749    ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n → u(n) ∈ U750  shows u ⇝ x751proof752  unfold Converges753  refine ⟨sequence, point, ?_⟩754  intros U hU hxU755  exact eventually with U, (Open.of_mem with hU), hxU756757-- A constant sequence converges to its value.758theorem Converges.constant (x : Set)759  requires point : x ∈ X760  shows constantFunction(ℕ, X.carrier, x) ⇝ x761proof762  have sequence := constantFunction.function at ℕ, X.carrier, x with point763  have eventually : ∀ U, Open(X, U) → x ∈ U →764      ∃ N ∈ ℕ, ∀ n ∈ ℕ, N ≤ n →765        apply(constantFunction(ℕ, X.carrier, x), n) ∈ U766    intros U open hxU767    have zeroIn : (0:N) ∈ ℕ by typecheck768    witness (0:N)769    refine ⟨zeroIn, ?_⟩770    intros n hn order771    have value := constantFunction.apply at ℕ, X.carrier, n, x with hn, point772    rw value773    exact hxU774  exact Converges.of_eventually with *775776end ConvergenceLaws777778-- Bridges for the remaining properties: each bundled-to-unbundled779-- direction is an instance, so `with *` reads the form over separate pieces780-- off the bundled hypothesis.781section PropertyBridges782variable (X : Set)783hypothesis space : TopologicalSpace(X)784785instance Compact.parts (A : Set)786  requires compact : Compact(X, A)787  shows IsCompact(X.carrier, X.opens, A)788proof789  unfold Compact at compact790  exact compact791792theorem Compact.of_parts (A : Set)793  requires compact : IsCompact(X.carrier, X.opens, A)794  shows Compact(X, A)795proof796  unfold Compact797  exact compact798799instance ConnectedSubset.parts (A : Set)800  requires connected : ConnectedSubset(X, A)801  shows IsConnectedSubset(X.carrier, X.opens, A)802proof803  unfold ConnectedSubset at connected804  exact connected805806theorem ConnectedSubset.of_parts (A : Set)807  requires connected : IsConnectedSubset(X.carrier, X.opens, A)808  shows ConnectedSubset(X, A)809proof810  unfold ConnectedSubset811  exact connected812813end PropertyBridges814815instance Compact.space_parts (X : Set)816  requires compact : Compact(X)817  shows IsCompact(X.carrier, X.opens, X.carrier)818proof819  unfold Compact at compact820  exact compact821822theorem Compact.of_space_parts (X : Set)823  requires compact : IsCompact(X.carrier, X.opens, X.carrier)824  shows Compact(X)825proof826  unfold Compact827  exact compact828829instance Hausdorff.parts (X : Set)830  requires hausdorff : Hausdorff(X)831  shows IsHausdorff(X.carrier, X.opens)832proof833  unfold Hausdorff at hausdorff834  exact hausdorff835836theorem Hausdorff.of_parts (X : Set)837  requires hausdorff : IsHausdorff(X.carrier, X.opens)838  shows Hausdorff(X)839proof840  unfold Hausdorff841  exact hausdorff842843instance T1Space.parts (X : Set)844  requires t1 : T1Space(X)845  shows IsT1Space(X.carrier, X.opens)846proof847  unfold T1Space at t1848  exact t1849850theorem T1Space.of_parts (X : Set)851  requires t1 : IsT1Space(X.carrier, X.opens)852  shows T1Space(X)853proof854  unfold T1Space855  exact t1856857instance Connected.parts (X : Set)858  requires connected : Connected(X)859  shows IsConnected(X.carrier, X.opens)860proof861  unfold Connected at connected862  exact connected863864theorem Connected.of_parts (X : Set)865  requires connected : IsConnected(X.carrier, X.opens)866  shows Connected(X)867proof868  unfold Connected869  exact connected870871-- The same bridges for a constructed space: a fact over the pieces (A, T)872-- is the bundled fact at TopologicalSpace.mk(A, T).873theorem Open.of_mk (A T U : Set)874  requires topology : IsTopology(A, T)875  requires member : U ∈ T876  shows Open(TopologicalSpace.mk(A, T), U)877proof878  have space := TopologicalSpace.of_parts with topology879  have shifted : U ∈ TopologicalSpace.opens(TopologicalSpace.mk(A, T))880    topology_projections881  exact Open.of_mem with space, shifted882883theorem Closed.of_mk (A T C : Set)884  requires topology : IsTopology(A, T)885  requires closed : IsClosed(A, T, C)886  shows Closed(TopologicalSpace.mk(A, T), C)887proof888  have space := TopologicalSpace.of_parts with topology889  have shifted : IsClosed(TopologicalSpace.carrier(TopologicalSpace.mk(A, T)),890      TopologicalSpace.opens(TopologicalSpace.mk(A, T)), C)891    topology_projections892  exact Closed.of_parts with space, shifted893894theorem Compact.of_mk (A T S : Set)895  requires topology : IsTopology(A, T)896  requires compact : IsCompact(A, T, S)897  shows Compact(TopologicalSpace.mk(A, T), S)898proof899  have space := TopologicalSpace.of_parts with topology900  have shifted : IsCompact(TopologicalSpace.carrier(TopologicalSpace.mk(A, T)),901      TopologicalSpace.opens(TopologicalSpace.mk(A, T)), S)902    topology_projections903  exact Compact.of_parts with space, shifted904905theorem ConnectedSubset.of_mk (A T S : Set)906  requires topology : IsTopology(A, T)907  requires connected : IsConnectedSubset(A, T, S)908  shows ConnectedSubset(TopologicalSpace.mk(A, T), S)909proof910  have space := TopologicalSpace.of_parts with topology911  have shifted : IsConnectedSubset(912      TopologicalSpace.carrier(TopologicalSpace.mk(A, T)),913      TopologicalSpace.opens(TopologicalSpace.mk(A, T)), S)914    topology_projections915  exact ConnectedSubset.of_parts with space, shifted916917theorem Hausdorff.of_mk (A T : Set)918  requires hausdorff : IsHausdorff(A, T)919  shows Hausdorff(TopologicalSpace.mk(A, T))920proof921  unfold Hausdorff922  topology_projections923924theorem T1Space.of_mk (A T : Set)925  requires t1 : IsT1Space(A, T)926  shows T1Space(TopologicalSpace.mk(A, T))927proof928  unfold T1Space929  topology_projections930931theorem Connected.of_mk (A T : Set)932  requires connected : IsConnected(A, T)933  shows Connected(TopologicalSpace.mk(A, T))934proof935  unfold Connected936  topology_projections937938theorem Compact.of_space_mk (A T : Set)939  requires compact : IsCompact(A, T, A)940  shows Compact(TopologicalSpace.mk(A, T))941proof942  unfold Compact943  topology_projections944