Grace/Cumulus/Topology/Connected.g17

Open in Workbench Download source

Imports

Separation

Declarations

Source

1-- Connectedness: a space with no splitting into two disjoint nonempty open2-- sets, connected subsets through open separations, the clopen3-- characterisation, examples, continuous images, closures, unions through4-- a common point, and connected components5-- 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.Connected11import Separation1213-- A disconnection of the space; an open separation of a subset A uses two14-- open sets whose traces on A are disjoint, nonempty, and cover A.15predicate Disconnection (X T U V : Set) :=16  U ∈ T ∧ V ∈ T ∧ Nonempty(U) ∧ Nonempty(V) ∧ Disjoint(U, V) ∧ U ∪ V = X1718predicate OpenSeparation (T A U V : Set) :=19  U ∈ T ∧ V ∈ T ∧ A ⊆ U ∪ V ∧ Disjoint(U ∩ A, V ∩ A) ∧20  Nonempty(U ∩ A) ∧ Nonempty(V ∩ A)2122predicate IsConnected (X T : Set) := ¬(∃ U, ∃ V, Disconnection(X, T, U, V))2324predicate IsConnectedSubset (X T A : Set) :=25  A ⊆ X ∧ ¬(∃ U, ∃ V, OpenSeparation(T, A, U, V))2627theorem IsConnectedSubset.subset (X T A : Set)28  requires connected : IsConnectedSubset(X, T, A)29  shows A ⊆ X30proof31  exact connected.left3233theorem IsConnectedSubset.no_separation (X T A U V : Set)34  requires connected : IsConnectedSubset(X, T, A)35  requires separation : OpenSeparation(T, A, U, V)36  shows ⊥37proof38  apply connected.right39  exact ⟨U, V, separation⟩4041theorem OpenSeparation.symmetric (T A U V : Set)42  requires separation : OpenSeparation(T, A, U, V)43  shows OpenSeparation(T, A, V, U)44proof45  obtain ⟨hU, hV, covers, disjoint, inhabitedU, inhabitedV⟩ := separation46  have swapped : A ⊆ V ∪ U47    rw union2.commutative48    exact covers49  exact ⟨hV, hU, swapped, (Disjoint.symmetric with disjoint), inhabitedV, inhabitedU⟩5051-- The clopen characterisation.5253theorem IsConnected.clopen (X T U : Set)54  requires topology : IsTopology(X, T)55  requires connected : IsConnected(X, T)56  requires isOpen : U ∈ T57  requires closed : IsClosed(X, T, U)58  shows U = ∅ ∨ U = X59proof60  have hUX := closed.left61  by_contra neither62  have notEmpty : U ≠ ∅63    intro equal64    apply neither65    left66    exact equal67  have notWhole : U ≠ X68    intro equal69    apply neither70    right71    exact equal72  have negation : ¬(∃ U, ∃ V, Disconnection(X, T, U, V)) := connected73  apply negation74  witness U75  witness complement(X, U)76  refine ⟨isOpen, closed.right, (Nonempty.of_ne_empty with notEmpty), ?_, ?_, (complement.union2 with hUX)⟩77  . by_contra none78    apply notWhole79    apply Subset.antisymmetric80    . exact hUX81    . intros x hx82      by_contra outside83      apply none84      witness x85      exact complement.membership.backward with ⟨hx, outside⟩86  . have same := complement.intersection at X, U87    exact same8889theorem IsConnected.of_clopen (X T : Set)90  requires topology : IsTopology(X, T)91  requires trivial : ∀ U ∈ T, IsClosed(X, T, U) → U = ∅ ∨ U = X92  shows IsConnected(X, T)93proof94  unfold IsConnected95  intro split96  obtain ⟨U, V, hU, hV, inhabitedU, inhabitedV, disjoint, whole⟩ := split97  have hUX := IsTopology.subset with topology, hU98  have hVX := IsTopology.subset with topology, hV99  have separated := Disjoint.iff.forward with disjoint100  have complementV : complement(X, U) = V101    ext x102    constructor103    . intro hx104      have parts := complement.membership.forward with hx105      have hxX := parts.left106      rw ← whole at hxX107      have split2 := union2.membership.forward with hxX108      cases split2 with inU | inV109      . exfalso110        exact parts.right with inU111      . exact inV112    . intro hx113      apply complement.membership.backward114      refine ⟨(hVX with x, hx), ?_⟩115      intro inU116      exact separated with x, inU, hx117  have closedU : IsClosed(X, T, U)118    constructor119    . exact hUX120    . rw complementV121      exact hV122  have cases := trivial with U, hU, closedU123  cases cases with isEmpty | isWhole124  . obtain ⟨x, hx⟩ := inhabitedU125    rw isEmpty at hx126    exact empty.membership with x, hx127  . obtain ⟨y, hy⟩ := inhabitedV128    have hyU : y ∈ U129      rw isWhole130      exact hVX with y, hy131    exact separated with y, hyU, hy132133theorem IsConnected.iff_clopen (X T : Set)134  requires topology : IsTopology(X, T)135  shows IsConnected(X, T) ↔ ∀ U ∈ T, IsClosed(X, T, U) → U = ∅ ∨ U = X136proof137  constructor138  . intros connected U hU closed139    exact IsConnected.clopen with topology, connected, hU, closed140  . intro trivial141    exact IsConnected.of_clopen with topology, trivial142143-- Examples: the indiscrete space is connected; a discrete two-point space144-- is not.145146theorem IsConnected.indiscrete (X : Set)147  shows IsConnected(X, {∅, X})148proof149  unfold IsConnected150  intro split151  obtain ⟨U, V, hU, hV, inhabitedU, inhabitedV, disjoint, whole⟩ := split152  have separated := Disjoint.iff.forward with disjoint153  obtain ⟨x, hx⟩ := inhabitedU154  obtain ⟨y, hy⟩ := inhabitedV155  have splitU := pair.membership.forward with hU156  have splitV := pair.membership.forward with hV157  cases splitU with emptyU | wholeU158  . rw emptyU at hx159    exact empty.membership with x, hx160  . cases splitV with emptyV | wholeV161    . rw emptyV at hy162      exact empty.membership with y, hy163    . have hxV : x ∈ V164        rw [wholeV, ← wholeU]165        exact hx166      exact separated with x, hx, hxV167168theorem IsConnected.not_discrete_pair (a b : Set)169  requires distinct : a ≠ b170  shows ¬IsConnected({a, b}, 𝒫({a, b}))171proof172  intro connected173  have negation : ¬(∃ U, ∃ V, Disconnection({a, b}, 𝒫({a, b}), U, V)) := connected174  apply negation175  have singletonA : {a} ⊆ {a, b} := singleton.subset_pair at a, b176  have singletonB : {b} ⊆ {a, b}177    intros z hz178    have same := singleton.membership.forward with hz179    rw same180    exact pair.right at a, b181  witness {a}182  witness {b}183  refine ⟨(powerset.membership_iff.backward with singletonA), (powerset.membership_iff.backward with singletonB), (Nonempty.singleton at a), (Nonempty.singleton at b), ?_, ?_⟩184  . apply Disjoint.iff.backward185    intros z hz hz2186    have sameA := singleton.membership.forward with hz187    have sameB := singleton.membership.forward with hz2188    apply distinct189    rw [← sameA, ← sameB]190    rfl191  . symm192    exact pair.eq_union2 at a, b193194-- The whole space is a connected subset exactly when the space is195-- connected.196197theorem IsConnectedSubset.whole_iff (X T : Set)198  requires topology : IsTopology(X, T)199  shows IsConnectedSubset(X, T, X) ↔ IsConnected(X, T)200proof201  constructor202  . intros connected split203    obtain ⟨U, V, hU, hV, inhabitedU, inhabitedV, disjoint, whole⟩ := split204    have hUX := IsTopology.subset with topology, hU205    have hVX := IsTopology.subset with topology, hV206    have traceU := intersection.eq_left_of_subset with hUX207    have traceV := intersection.eq_left_of_subset with hVX208    apply connected.right209    witness U210    witness V211    refine ⟨hU, hV, ?_, ?_, ?_, ?_⟩212    . rw whole213      exact Subset.reflexive at X214    . rw [traceU, traceV]215      exact disjoint216    . rw traceU217      exact inhabitedU218    . rw traceV219      exact inhabitedV220  . intro connected221    constructor222    . exact Subset.reflexive at X223    . intro split224      obtain ⟨U, V, hU, hV, covers, disjoint, inhabitedU, inhabitedV⟩ := split225      have hUX := IsTopology.subset with topology, hU226      have hVX := IsTopology.subset with topology, hV227      have traceU := intersection.eq_left_of_subset with hUX228      have traceV := intersection.eq_left_of_subset with hVX229      rw [traceU, traceV] at disjoint230      rw traceU at inhabitedU231      rw traceV at inhabitedV232      have negation : ¬(∃ U, ∃ V, Disconnection(X, T, U, V)) := connected233      apply negation234      witness U235      witness V236      refine ⟨hU, hV, inhabitedU, inhabitedV, disjoint, ?_⟩237      exact Subset.antisymmetric with (union2.subset with hUX, hVX), covers238239theorem IsConnectedSubset.empty (X T : Set)240  shows IsConnectedSubset(X, T, ∅)241proof242  constructor243  . exact empty.subset at X244  . intro split245    obtain ⟨U, V, hU, hV, covers, disjoint, inhabitedU, inhabitedV⟩ := split246    obtain ⟨x, hx⟩ := inhabitedU247    have parts := intersection.membership.forward with hx248    exact empty.membership with x, parts.right249250theorem IsConnectedSubset.singleton (X T x : Set)251  requires hx : x ∈ X252  shows IsConnectedSubset(X, T, {x})253proof254  constructor255  . exact singleton.subset_iff.backward with hx256  . intro split257    obtain ⟨U, V, hU, hV, covers, disjoint, inhabitedU, inhabitedV⟩ := split258    have separated := Disjoint.iff.forward with disjoint259    obtain ⟨y, hy⟩ := inhabitedU260    obtain ⟨z, hz⟩ := inhabitedV261    have partsY := intersection.membership.forward with hy262    have partsZ := intersection.membership.forward with hz263    have sameY := singleton.membership.forward with partsY.right264    have sameZ := singleton.membership.forward with partsZ.right265    rw sameY at hy266    rw sameZ at hz267    exact separated with x, hy, hz268269-- A connected subset meeting one side of a would-be separation lies in it.270theorem IsConnectedSubset.absorbed (X T A U V x : Set)271  requires connected : IsConnectedSubset(X, T, A)272  requires hU : U ∈ T273  requires hV : V ∈ T274  requires covers : A ⊆ U ∪ V275  requires disjoint : Disjoint(U ∩ A, V ∩ A)276  requires hxA : x ∈ A277  requires hxU : x ∈ U278  shows A ⊆ U279proof280  intros a ha281  by_contra outside282  have inUnion := covers with a, ha283  have split := union2.membership.forward with inUnion284  cases split with inU | inV285  . exact outside with inU286  . apply connected.right287    have inhabitedU : Nonempty(U ∩ A) := ⟨x, (intersection.membership.backward with ⟨hxU, hxA⟩)⟩288    have inhabitedV : Nonempty(V ∩ A) := ⟨a, (intersection.membership.backward with ⟨inV, ha⟩)⟩289    witness U290    witness V291    exact ⟨hU, hV, covers, disjoint, inhabitedU, inhabitedV⟩292293-- The continuous image of a connected subset is connected.294theorem IsConnectedSubset.image (f X T Y S A : Set)295  requires continuous : ContinuousMap(f, X, T, Y, S)296  requires connected : IsConnectedSubset(X, T, A)297  shows IsConnectedSubset(Y, S, functionImage(f, A, Y))298proof299  have function := continuous.left300  have hAX := connected.left301  constructor302  . exact functionImage.subset at f, A, Y303  . intro split304    obtain ⟨U, V, hU, hV, covers, disjoint, inhabitedU, inhabitedV⟩ := split305    have separated := Disjoint.iff.forward with disjoint306    have openU := continuous.right with U, hU307    have openV := continuous.right with V, hV308    apply connected.right309    witness functionPreimage(f, X, U)310    witness functionPreimage(f, X, V)311    refine ⟨openU, openV, ?_, ?_, ?_, ?_⟩312    . intros a ha313      have haX := hAX with a, ha314      have valueY := FunctionBetween.apply_closed with function, haX315      have imageMember : f(a) ∈ functionImage(f, A, Y) by simp [functionImage.membership]316      have inUnion := covers with f(a), imageMember317      have split2 := union2.membership.forward with inUnion318      apply union2.membership.backward319      cases split2 with inU | inV320      . left321        exact functionPreimage.membership.backward with ⟨haX, inU⟩322      . right323        exact functionPreimage.membership.backward with ⟨haX, inV⟩324    . apply Disjoint.iff.backward325      intros a haU haV326      have partsU := intersection.membership.forward with haU327      have partsV := intersection.membership.forward with haV328      have valueU := functionPreimage.membership.forward with partsU.left329      have valueV := functionPreimage.membership.forward with partsV.left330      have haX := hAX with a, partsU.right331      have valueY := FunctionBetween.apply_closed with function, haX332      have imageMember : f(a) ∈ functionImage(f, A, Y) by simp [functionImage.membership]333      have inTraceU : f(a) ∈ U ∩ functionImage(f, A, Y) := intersection.membership.backward with ⟨valueU.right, imageMember⟩334      have inTraceV : f(a) ∈ V ∩ functionImage(f, A, Y) := intersection.membership.backward with ⟨valueV.right, imageMember⟩335      exact separated with f(a), inTraceU, inTraceV336    . obtain ⟨y, hy⟩ := inhabitedU337      have parts := intersection.membership.forward with hy338      have hyU := parts.left339      have imageParts := functionImage.membership.forward with parts.right340      obtain ⟨hyY, a, ha, shape⟩ := imageParts341      have haX := hAX with a, ha342      rw shape at hyU343      witness a344      exact intersection.membership.backward with ⟨(functionPreimage.membership.backward with ⟨haX, hyU⟩), ha⟩345    . obtain ⟨y, hy⟩ := inhabitedV346      have parts := intersection.membership.forward with hy347      have hyV := parts.left348      have imageParts := functionImage.membership.forward with parts.right349      obtain ⟨hyY, a, ha, shape⟩ := imageParts350      have haX := hAX with a, ha351      rw shape at hyV352      witness a353      exact intersection.membership.backward with ⟨(functionPreimage.membership.backward with ⟨haX, hyV⟩), ha⟩354355theorem IsConnected.image (f X T Y S : Set)356  requires topology : IsTopology(X, T)357  requires continuous : ContinuousMap(f, X, T, Y, S)358  requires connected : IsConnected(X, T)359  shows IsConnectedSubset(Y, S, functionImage(f, X, Y))360proof361  have whole := IsConnectedSubset.whole_iff.backward with topology, connected362  exact IsConnectedSubset.image with continuous, whole363364-- A continuous surjection carries connectedness to the codomain.365theorem IsConnected.of_surjection (f X T Y S : Set)366  requires topologyX : IsTopology(X, T)367  requires topologyY : IsTopology(Y, S)368  requires continuous : ContinuousMap(f, X, T, Y, S)369  requires surjective : SurjectiveBetween(f, X, Y)370  requires connected : IsConnected(X, T)371  shows IsConnected(Y, S)372proof373  have function := continuous.left374  have image := IsConnected.image with topologyX, continuous, connected375  have whole : functionImage(f, X, Y) = Y376    apply Subset.antisymmetric377    . exact functionImage.subset at f, X, Y378    . intros y hy379      obtain ⟨x, hx, edge⟩ := surjective.right with y, hy380      have value := FunctionBetween.apply_value with function, hx, edge381      rw ← value382      exact functionImage.value with function, hx383  rw whole at image384  exact IsConnectedSubset.whole_iff.forward with topologyY, image385386theorem IsConnected.of_homeomorphism (f X T Y S : Set)387  requires topologyX : IsTopology(X, T)388  requires topologyY : IsTopology(Y, S)389  requires homeomorphism : IsHomeomorphism(f, X, T, Y, S)390  requires connected : IsConnected(X, T)391  shows IsConnected(Y, S)392proof393  obtain ⟨bijective, continuous, inverse⟩ := homeomorphism394  have surjective := Bijective.surjective with bijective395  exact IsConnected.of_surjection with topologyX, topologyY, continuous, surjective, connected396397theorem IsConnected.homeomorphic_iff (f X T Y S : Set)398  requires topologyX : IsTopology(X, T)399  requires topologyY : IsTopology(Y, S)400  requires homeomorphism : IsHomeomorphism(f, X, T, Y, S)401  shows IsConnected(X, T) ↔ IsConnected(Y, S)402proof403  have inverse := IsHomeomorphism.inverse with homeomorphism404  constructor405  . intro connected406    exact IsConnected.of_homeomorphism with topologyX, topologyY, homeomorphism, connected407  . intro connected408    exact IsConnected.of_homeomorphism with topologyY, topologyX, inverse, connected409410-- Anything between a connected set and its closure is connected.411theorem IsConnectedSubset.between (X T A B : Set)412  requires topology : IsTopology(X, T)413  requires connected : IsConnectedSubset(X, T, A)414  requires hAB : A ⊆ B415  requires hB : B ⊆ closure(X, T, A)416  shows IsConnectedSubset(X, T, B)417proof418  have hAX := connected.left419  have closureInside := closure.subset with topology, hAX420  constructor421  . exact Subset.transitive with hB, closureInside422  . intro split423    obtain ⟨U, V, hU, hV, covers, disjoint, inhabitedU, inhabitedV⟩ := split424    have separated := Disjoint.iff.forward with disjoint425    apply connected.right426    have meetsU : Nonempty(U ∩ A)427      obtain ⟨b, hb⟩ := inhabitedU428      have parts := intersection.membership.forward with hb429      have inClosure := hB with b, parts.right430      have touches := closure.membership.forward with topology, hAX, inClosure431      exact touches.right with U, hU, parts.left432    have meetsV : Nonempty(V ∩ A)433      obtain ⟨b, hb⟩ := inhabitedV434      have parts := intersection.membership.forward with hb435      have inClosure := hB with b, parts.right436      have touches := closure.membership.forward with topology, hAX, inClosure437      exact touches.right with V, hV, parts.left438    witness U439    witness V440    refine ⟨hU, hV, (Subset.transitive with hAB, covers), ?_, meetsU, meetsV⟩441    apply Disjoint.iff.backward442    intros a haU haV443    have partsU := intersection.membership.forward with haU444    have partsV := intersection.membership.forward with haV445    have inB := hAB with a, partsU.right446    have inTraceU : a ∈ U ∩ B := intersection.membership.backward with ⟨partsU.left, inB⟩447    have inTraceV : a ∈ V ∩ B := intersection.membership.backward with ⟨partsV.left, inB⟩448    exact separated with a, inTraceU, inTraceV449450theorem IsConnectedSubset.closure (X T A : Set)451  requires topology : IsTopology(X, T)452  requires connected : IsConnectedSubset(X, T, A)453  shows IsConnectedSubset(X, T, closure(X, T, A))454proof455  have contains := Space.closure.contains with topology, connected.left456  exact IsConnectedSubset.between with topology, connected, contains, (Subset.reflexive at closure(X, T, A))457458-- Unions of connected subsets through a common point are connected.459460theorem IsConnectedSubset.union_family (X T F p : Set)461  requires connected : ∀ A ∈ F, IsConnectedSubset(X, T, A)462  requires common : ∀ A ∈ F, p ∈ A463  shows IsConnectedSubset(X, T, ⋃(F))464proof465  constructor466  . apply union.subset467    intros A hA468    have connectedA := connected with A, hA469    exact connectedA.left470  . intro split471    obtain ⟨U, V, hU, hV, covers, disjoint, inhabitedU, inhabitedV⟩ := split472    have separated := Disjoint.iff.forward with disjoint473    have memberDisjoint : ∀ A ∈ F, Disjoint(U ∩ A, V ∩ A)474      intros A hA475      have below := union.subset_of_member with hA476      have leftBelow := intersection.monotone_right at A, ⋃(F), U with below477      have rightBelow := intersection.monotone_right at A, ⋃(F), V with below478      have first := Disjoint.of_subset_left with disjoint, leftBelow479      exact Disjoint.of_subset_right with first, rightBelow480    have memberCovers : ∀ A ∈ F, A ⊆ U ∪ V481      intros A hA482      exact Subset.transitive with (union.subset_of_member with hA), covers483    obtain ⟨x, hx⟩ := inhabitedU484    have partsX := intersection.membership.forward with hx485    obtain ⟨A0, hA0, hxA0⟩ := union.membership.forward with partsX.right486    have hpA0 := common with A0, hA0487    have hpUnion := union.contains with hA0, hpA0488    have hpUnionV := union.contains with hA0, hpA0489    have splitP := union2.membership.forward with (covers with p, hpUnion)490    cases splitP with inU | inV491    . have inside : ⋃(F) ⊆ U492        apply union.subset493        intros A hA494        exact IsConnectedSubset.absorbed with (connected with A, hA), hU, hV, (memberCovers with A, hA), (memberDisjoint with A, hA), (common with A, hA), inU495      obtain ⟨y, hy⟩ := inhabitedV496      have partsY := intersection.membership.forward with hy497      have hyU := inside with y, partsY.right498      have inTraceU : y ∈ U ∩ ⋃(F) := intersection.membership.backward with ⟨hyU, partsY.right⟩499      exact separated with y, inTraceU, hy500    . have inside : ⋃(F) ⊆ V501        apply union.subset502        intros A hA503        have swappedCovers : A ⊆ V ∪ U504          rw union2.commutative505          exact memberCovers with A, hA506        have swappedDisjoint := Disjoint.symmetric with (memberDisjoint with A, hA)507        exact IsConnectedSubset.absorbed with (connected with A, hA), hV, hU, swappedCovers, swappedDisjoint, (common with A, hA), inV508      have hxV := inside with x, partsX.right509      have inTraceV : x ∈ V ∩ ⋃(F) := intersection.membership.backward with ⟨hxV, partsX.right⟩510      exact separated with x, hx, inTraceV511512theorem IsConnectedSubset.union2 (X T A B : Set)513  requires connectedA : IsConnectedSubset(X, T, A)514  requires connectedB : IsConnectedSubset(X, T, B)515  requires meets : Nonempty(A ∩ B)516  shows IsConnectedSubset(X, T, A ∪ B)517proof518  obtain ⟨p, hp⟩ := meets519  have parts := intersection.membership.forward with hp520  have connected : ∀ C ∈ {A, B}, IsConnectedSubset(X, T, C)521    intros C hC522    have split := pair.membership.forward with hC523    cases split with isA | isB524    . rw isA525      exact connectedA526    . rw isB527      exact connectedB528  have common : ∀ C ∈ {A, B}, p ∈ C529    intros C hC530    have split := pair.membership.forward with hC531    cases split with isA | isB532    . rw isA533      exact parts.left534    . rw isB535      exact parts.right536  have joined := IsConnectedSubset.union_family with connected, common537  rwa union.pair at joined538539-- Connected components: the union of the connected subsets through a540-- point.541542def connectedThrough (X T x : Set) : Set :=543  { A ∈ 𝒫(X) | IsConnectedSubset(X, T, A) ∧ x ∈ A }544545def component (X T x : Set) : Set := ⋃(connectedThrough(X, T, x))546547theorem component.connected (X T x : Set)548  shows IsConnectedSubset(X, T, component(X, T, x))549proof550  unfold component551  apply IsConnectedSubset.union_family at X, T, connectedThrough(X, T, x), x552  . intros A hA553    have parts := connectedThrough.membership.forward with hA554    exact parts.right.left555  . intros A hA556    have parts := connectedThrough.membership.forward with hA557    exact parts.right.right558559theorem component.subset (X T x : Set)560  shows component(X, T, x) ⊆ X561proof562  have connected := component.connected at X, T, x563  exact connected.left564565theorem component.maximal (X T x A : Set)566  requires connected : IsConnectedSubset(X, T, A)567  requires hx : x ∈ A568  shows A ⊆ component(X, T, x)569proof570  have found : A ∈ connectedThrough(X, T, x)571    apply connectedThrough.membership.backward572    exact ⟨(powerset.membership_iff.backward with connected.left), connected, hx⟩573  unfold component574  exact union.subset_of_member with found575576theorem component.contains (X T x : Set)577  requires hx : x ∈ X578  shows x ∈ component(X, T, x)579proof580  have connected := IsConnectedSubset.singleton at X, T, x with hx581  have self : x ∈ {x} by simp [singleton.membership]582  have below := component.maximal with connected, self583  exact below with x, self584585theorem component.closed (X T x : Set)586  requires topology : IsTopology(X, T)587  requires hx : x ∈ X588  shows IsClosed(X, T, component(X, T, x))589proof590  have connected := component.connected at X, T, x591  have closureConnected := IsConnectedSubset.closure with topology, connected592  have contains := Space.closure.contains with topology, connected.left593  have hxClosure := contains with x, (component.contains with hx)594  have below := component.maximal with closureConnected, hxClosure595  apply IsClosed.iff_closure.backward with topology, connected.left596  exact Subset.antisymmetric with below, contains597598theorem component.eq_of_member (X T x y : Set)599  requires hx : x ∈ X600  requires hy : y ∈ component(X, T, x)601  shows component(X, T, y) = component(X, T, x)602proof603  have connectedX := component.connected at X, T, x604  have connectedY := component.connected at X, T, y605  have hyX := component.subset at X, T, x with y, hy606  have first := component.maximal with connectedX, hy607  have hxY := first with x, (component.contains with hx)608  have second := component.maximal with connectedY, hxY609  exact Subset.antisymmetric with second, first610611-- Connected subsets agree with connectedness of the subspace.612theorem IsConnectedSubset.iff_subspace (X T A : Set)613  requires topology : IsTopology(X, T)614  requires hA : A ⊆ X615  shows IsConnectedSubset(X, T, A) ↔ IsConnected(A, subspaceTopology(T, A))616proof617  constructor618  . intro connected619    unfold IsConnected620    intro split621    obtain ⟨U1, V1, hU1, hV1, inhabitedU, inhabitedV, disjoint, whole⟩ := split622    obtain ⟨U, hU, shapeU⟩ := subspaceTopology.membership.forward with hU1623    obtain ⟨V, hV, shapeV⟩ := subspaceTopology.membership.forward with hV1624    rw ← shapeU at inhabitedU625    rw ← shapeV at inhabitedV626    rw [← shapeU, ← shapeV] at disjoint627    rw [← shapeU, ← shapeV] at whole628    apply connected.right629    witness U630    witness V631    refine ⟨hU, hV, ?_, disjoint, inhabitedU, inhabitedV⟩632    intros a ha633    have inWhole : a ∈ U ∩ A ∪ V ∩ A634      rw whole635      exact ha636    have split2 := union2.membership.forward with inWhole637    apply union2.membership.backward638    cases split2 with inU | inV639    . left640      have parts := intersection.membership.forward with inU641      exact parts.left642    . right643      have parts := intersection.membership.forward with inV644      exact parts.left645  . intro connected646    constructor647    . exact hA648    . intro split649      obtain ⟨U, V, hU, hV, covers, disjoint, inhabitedU, inhabitedV⟩ := split650      have tracedU : U ∩ A ∈ subspaceTopology(T, A) := subspaceTopology.membership.backward with ⟨U, hU, rfl⟩651      have tracedV : V ∩ A ∈ subspaceTopology(T, A) := subspaceTopology.membership.backward with ⟨V, hV, rfl⟩652      have negation : ¬(∃ U, ∃ V, Disconnection(A, subspaceTopology(T, A), U, V)) := connected653      apply negation654      witness U ∩ A655      witness V ∩ A656      refine ⟨tracedU, tracedV, inhabitedU, inhabitedV, disjoint, ?_⟩657      apply Subset.antisymmetric658      . exact union2.subset with (intersection.subset_right at U, A), (intersection.subset_right at V, A)659      . intros a ha660        have split2 := union2.membership.forward with (covers with a, ha)661        apply union2.membership.backward662        cases split2 with inU | inV663        . left664          exact intersection.membership.backward with ⟨inU, ha⟩665        . right666          exact intersection.membership.backward with ⟨inV, ha⟩667