Grace/Cumulus/GraphTheory/Multigraph/Components.g17

Open in Workbench Download source

Imports

Connectivity · Cardinal.FiniteSubsets

Declarations

Source

1-- Components of an edge set: adding an edge joins at most two components,2-- a finite vertex set has at least |V| - |F| components and exactly one when3-- F connects it, and an even edge set joins the ends of each of its edges.4-- 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.GraphTheory.Multigraph.Components10import Connectivity11import Cardinal.FiniteSubsets1213-- Components. A vertex lies in its own component, two vertices with the same14-- component are joined, and the components are finitely many subsets of V.15theorem componentBy.self (V leftEnd rightEnd F u : Set)16  requires vertex : u ∈ V17  shows u ∈ componentBy(V, leftEnd, rightEnd, F, u)18proof19  exact ⟨vertex, Joined.reflexive⟩2021theorem componentBy.joined (V leftEnd rightEnd F u v : Set)22  requires member : v ∈ componentBy(V, leftEnd, rightEnd, F, u)23  shows Joined(leftEnd, rightEnd, F, u, v)24proof25  exact member.right2627theorem componentBy.subset (V leftEnd rightEnd F u : Set)28  shows componentBy(V, leftEnd, rightEnd, F, u) ⊆ V29proof30  intros w hw31  exact hw.left3233-- Components grow with the edge set.34theorem componentBy.monotone (V leftEnd rightEnd F G u : Set)35  requires subset : F ⊆ G36  shows componentBy(V, leftEnd, rightEnd, F, u) ⊆37    componentBy(V, leftEnd, rightEnd, G, u)38proof39  intros v hv40  exact ⟨hv.left, (Joined.monotone with subset, hv.right)⟩4142theorem componentBy.joined_of_eq (V leftEnd rightEnd F u v : Set)43  requires vertex : v ∈ V44  requires same : componentBy(V, leftEnd, rightEnd, F, u) =45    componentBy(V, leftEnd, rightEnd, F, v)46  shows Joined(leftEnd, rightEnd, F, u, v)47proof48  have self := componentBy.self at V, leftEnd, rightEnd, F, v with vertex49  rw ← same at self50  exact self.right5152theorem componentBy.eq_iff_joined (V leftEnd rightEnd F u v : Set)53  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V54  requires first : u ∈ V55  requires second : v ∈ V56  shows componentBy(V, leftEnd, rightEnd, F, u) =57    componentBy(V, leftEnd, rightEnd, F, v)58    ↔ Joined(leftEnd, rightEnd, F, u, v)59proof60  constructor61  . intro same62    exact componentBy.joined_of_eq with second, same63  . intro joined64    exact componentBy.eq_of_joined with ends, first, second, joined6566theorem componentsBy.contains (V leftEnd rightEnd F u : Set)67  requires vertex : u ∈ V68  shows componentBy(V, leftEnd, rightEnd, F, u) ∈69    componentsBy(V, leftEnd, rightEnd, F)70proof71  exact ⟨u, vertex, rfl⟩7273theorem componentsBy.subset_powerset (V leftEnd rightEnd F : Set)74  shows componentsBy(V, leftEnd, rightEnd, F) ⊆ 𝒫(V)75proof76  intros X hX77  obtain ⟨u, hu, rfl⟩ := hX78  exact powerset.membership_iff.backward with componentBy.subset7980theorem componentsBy.finite (V leftEnd rightEnd F : Set)81  requires finiteVertices : Finite(V)82  shows Finite(componentsBy(V, leftEnd, rightEnd, F))83proof84  exact Finite.subset with85    (Finite.powerset with finiteVertices), componentsBy.subset_powerset8687-- Ends stay in V under passing to a subset and under adding an edge with88-- ends in V.89theorem ends_in.subset (V leftEnd rightEnd F G : Set)90  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V91  requires subset : G ⊆ F92  shows ∀ e ∈ G, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V93proof94  intros e he95  exact ends with e, (subset with e, he)9697theorem ends_in.union_edge (V leftEnd rightEnd F e : Set)98  requires ends : ∀ f ∈ F, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V99  requires edgeEnds : leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V100  shows ∀ f ∈ F ∪ {e}, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V101proof102  intros f hf103  simp at hf104  rcases hf with inF | rfl105  . exact ends with f, inF106  . exact edgeEnds107108-- A set closed under F holds both ends of an edge whose ends F joins, or109-- neither; so it stays closed when that edge is added.110theorem Joined.balanced (V leftEnd rightEnd F A u v : Set)111  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V112  requires first : u ∈ V113  requires second : v ∈ V114  requires joined : Joined(leftEnd, rightEnd, F, u, v)115  requires closed : ClosedUnder(leftEnd, rightEnd, F, A)116  shows u ∈ A ↔ v ∈ A117proof118  have back := Joined.symmetric with ends, first, second, joined119  constructor120  . intro hu121    exact joined with A, hu, closed122  . intro hv123    exact back with A, hv, closed124125theorem ClosedUnder.add_edge (leftEnd rightEnd F g A : Set)126  requires closed : ClosedUnder(leftEnd, rightEnd, F, A)127  requires balanced : leftEnd(g) ∈ A ↔ rightEnd(g) ∈ A128  shows ClosedUnder(leftEnd, rightEnd, F ∪ {g}, A)129proof130  intros e he131  simp at he132  rcases he with inF | rfl133  . exact closed with e, inF134  . exact balanced135136-- An edge whose ends F already joins adds nothing to connectivity.137theorem Joined.drop_edge (V leftEnd rightEnd F g u v : Set)138  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V139  requires edgeEnds : leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V140  requires joined : Joined(leftEnd, rightEnd, F ∪ {g}, u, v)141  requires bridged : Joined(leftEnd, rightEnd, F, leftEnd(g), rightEnd(g))142  shows Joined(leftEnd, rightEnd, F, u, v)143proof144  intros A hu closed145  have balanced := Joined.balanced with146    ends, edgeEnds.left, edgeEnds.right, bridged, closed147  exact joined with A, hu, (ClosedUnder.add_edge with closed, balanced)148149-- A vertex joined by F to neither end of e is joined by F ∪ {e} only to150-- what F joins it to: its F-component is closed under the new edge.151theorem Joined.drop_edge_apart (V leftEnd rightEnd F e u v : Set)152  requires ends : ∀ f ∈ F, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V153  requires vertex : u ∈ V154  requires apartLeft : ¬Joined(leftEnd, rightEnd, F, u, leftEnd(e))155  requires apartRight : ¬Joined(leftEnd, rightEnd, F, u, rightEnd(e))156  requires joined : Joined(leftEnd, rightEnd, F ∪ {e}, u, v)157  shows Joined(leftEnd, rightEnd, F, u, v)158proof159  have closed := componentBy.closed at V, leftEnd, rightEnd, F, u with ends160  have leftOut : ¬leftEnd(e) ∈ componentBy(V, leftEnd, rightEnd, F, u)161    intro member162    exact apartLeft with member.right163  have rightOut : ¬rightEnd(e) ∈ componentBy(V, leftEnd, rightEnd, F, u)164    intro member165    exact apartRight with member.right166  have balanced : leftEnd(e) ∈ componentBy(V, leftEnd, rightEnd, F, u) ↔167      rightEnd(e) ∈ componentBy(V, leftEnd, rightEnd, F, u) by tauto168  have self := componentBy.self at V, leftEnd, rightEnd, F, u with vertex169  have member := joined with componentBy(V, leftEnd, rightEnd, F, u), self,170    (ClosedUnder.add_edge with closed, balanced)171  exact member.right172173-- Once e is added, a vertex is apart from an end of e exactly when it was174-- apart from both ends before.175theorem Joined.add_edge_apart_iff (V leftEnd rightEnd F e w : Set)176  requires ends : ∀ f ∈ F, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V177  requires vertex : w ∈ V178  shows ¬Joined(leftEnd, rightEnd, F ∪ {e}, w, leftEnd(e)) ↔179    ¬Joined(leftEnd, rightEnd, F, w, leftEnd(e))180    ∧ ¬Joined(leftEnd, rightEnd, F, w, rightEnd(e))181proof182  have edge : e ∈ F ∪ {e} by simp183  have back : Joined(leftEnd, rightEnd, F ∪ {e}, rightEnd(e), leftEnd(e)) :=184    Joined.of_edge_reverse with edge185  constructor186  . intro apartMore187    constructor188    . intro joined189      exact apartMore with (Joined.monotone with union2.subset_left, joined)190    . intro joined191      have more : Joined(leftEnd, rightEnd, F ∪ {e}, w, rightEnd(e)) :=192        Joined.monotone with union2.subset_left, joined193      exact apartMore with (Joined.transitive with more, back)194  . intros both joinedMore195    exact both.left with (Joined.drop_edge_apart with196      ends, vertex, both.left, both.right, joinedMore)197198-- Adding an edge changes no component away from its ends, and none at all199-- when its ends were already joined.200theorem componentBy.add_edge_apart (V leftEnd rightEnd F e u : Set)201  requires ends : ∀ f ∈ F, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V202  requires vertex : u ∈ V203  requires apartLeft : ¬Joined(leftEnd, rightEnd, F, u, leftEnd(e))204  requires apartRight : ¬Joined(leftEnd, rightEnd, F, u, rightEnd(e))205  shows componentBy(V, leftEnd, rightEnd, F ∪ {e}, u) =206    componentBy(V, leftEnd, rightEnd, F, u)207proof208  apply Subset.antisymmetric209  . intros v hv210    have joined := Joined.drop_edge_apart with211      ends, vertex, apartLeft, apartRight, hv.right212    exact ⟨hv.left, joined⟩213  . exact componentBy.monotone with union2.subset_left214215theorem componentBy.add_edge_joined (V leftEnd rightEnd F e u : Set)216  requires ends : ∀ f ∈ F, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V217  requires edgeEnds : leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V218  requires bridged : Joined(leftEnd, rightEnd, F, leftEnd(e), rightEnd(e))219  shows componentBy(V, leftEnd, rightEnd, F ∪ {e}, u) =220    componentBy(V, leftEnd, rightEnd, F, u)221proof222  apply Subset.antisymmetric223  . intros v hv224    have joined := Joined.drop_edge with ends, edgeEnds, hv.right, bridged225    exact ⟨hv.left, joined⟩226  . exact componentBy.monotone with union2.subset_left227228-- When the ends of e are apart, the component of a vertex survives adding e229-- exactly when the vertex is apart from both ends: otherwise the new edge230-- would bring the other end into the component, joining the ends by F.231theorem componentBy.add_edge_unchanged (V leftEnd rightEnd F e w : Set)232  requires ends : ∀ f ∈ F, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V233  requires edgeEnds : leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V234  requires apart : ¬Joined(leftEnd, rightEnd, F, leftEnd(e), rightEnd(e))235  requires vertex : w ∈ V236  shows componentBy(V, leftEnd, rightEnd, F ∪ {e}, w) =237      componentBy(V, leftEnd, rightEnd, F, w)238    ↔ ¬Joined(leftEnd, rightEnd, F, w, leftEnd(e))239      ∧ ¬Joined(leftEnd, rightEnd, F, w, rightEnd(e))240proof241  constructor242  . intro same243    have apartMore : ¬Joined(leftEnd, rightEnd, F ∪ {e}, w, leftEnd(e))244      intro joinedMore245      have edge : e ∈ F ∪ {e} by simp246      have across :247          Joined(leftEnd, rightEnd, F ∪ {e}, leftEnd(e), rightEnd(e)) :=248        Joined.of_edge with edge249      have leftIn :250          leftEnd(e) ∈ componentBy(V, leftEnd, rightEnd, F ∪ {e}, w) :=251        ⟨edgeEnds.left, joinedMore⟩252      have rightIn :253          rightEnd(e) ∈ componentBy(V, leftEnd, rightEnd, F ∪ {e}, w) :=254        ⟨edgeEnds.right, (Joined.transitive with joinedMore, across)⟩255      rw same at leftIn256      rw same at rightIn257      have turn := Joined.symmetric with258        ends, vertex, edgeEnds.left, leftIn.right259      exact apart with (Joined.transitive with turn, rightIn.right)260    exact Joined.add_edge_apart_iff.forward with ends, vertex, apartMore261  . intro both262    exact componentBy.add_edge_apart with ends, vertex, both.left, both.right263264-- The components of an edge set are determined by the component of each265-- vertex.266theorem componentsBy.congr (V leftEnd rightEnd F G : Set)267  requires same : ∀ u ∈ V, componentBy(V, leftEnd, rightEnd, F, u) =268    componentBy(V, leftEnd, rightEnd, G, u)269  shows componentsBy(V, leftEnd, rightEnd, F) =270    componentsBy(V, leftEnd, rightEnd, G)271proof272  ext X273  constructor274  . intro hX275    obtain ⟨u, hu, rfl⟩ := hX276    have keep := same with u, hu277    rw keep278    exact componentsBy.contains with hu279  . intro hX280    obtain ⟨u, hu, rfl⟩ := hX281    have keep := same with u, hu282    rw ← keep283    exact componentsBy.contains with hu284285theorem componentsBy.add_edge_joined (V leftEnd rightEnd F e : Set)286  requires ends : ∀ f ∈ F, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V287  requires edgeEnds : leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V288  requires bridged : Joined(leftEnd, rightEnd, F, leftEnd(e), rightEnd(e))289  shows componentsBy(V, leftEnd, rightEnd, F ∪ {e}) =290    componentsBy(V, leftEnd, rightEnd, F)291proof292  apply componentsBy.congr293  intros u hu294  exact componentBy.add_edge_joined with ends, edgeEnds, bridged295296-- Adding an edge between two different components merges them and leaves297-- every other component alone, so the number of components drops by one.298theorem componentsBy.add_edge_apart (V leftEnd rightEnd F e : Set)299  requires finiteVertices : Finite(V)300  requires ends : ∀ f ∈ F, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V301  requires edgeEnds : leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V302  requires apart : ¬Joined(leftEnd, rightEnd, F, leftEnd(e), rightEnd(e))303  shows cardinality(componentsBy(V, leftEnd, rightEnd, F ∪ {e})) + 1 =304    cardinality(componentsBy(V, leftEnd, rightEnd, F))305proof306  have moreEnds := ends_in.union_edge with ends, edgeEnds307  have leftIn := componentsBy.contains at V, leftEnd, rightEnd, F, leftEnd(e)308    with edgeEnds.left309  have rightIn := componentsBy.contains at V, leftEnd, rightEnd, F,310    rightEnd(e) with edgeEnds.right311  have mergedIn := componentsBy.contains at V, leftEnd, rightEnd, F ∪ {e},312    leftEnd(e) with edgeEnds.left313  have different : componentBy(V, leftEnd, rightEnd, F, rightEnd(e)) ≠314      componentBy(V, leftEnd, rightEnd, F, leftEnd(e))315    intro same316    symm at same317    exact apart with (componentBy.joined_of_eq with edgeEnds.right, same)318  -- Away from the two components of the ends, nothing changes.319  have rest : (componentsBy(V, leftEnd, rightEnd, F) ∖320        {componentBy(V, leftEnd, rightEnd, F, leftEnd(e))}) ∖321        {componentBy(V, leftEnd, rightEnd, F, rightEnd(e))} =322      componentsBy(V, leftEnd, rightEnd, F ∪ {e}) ∖323        {componentBy(V, leftEnd, rightEnd, F ∪ {e}, leftEnd(e))}324    ext X325    constructor326    . intro hX327      simp at hX328      obtain ⟨⟨inOld, notLeft⟩, notRight⟩ := hX329      obtain ⟨w, hw, rfl⟩ := inOld330      rw (componentBy.eq_iff_joined with ends, hw, edgeEnds.left) at notLeft331      rw (componentBy.eq_iff_joined with ends, hw, edgeEnds.right) at notRight332      have keep := (componentBy.add_edge_unchanged with333        ends, edgeEnds, apart, hw).backward with ⟨notLeft, notRight⟩334      have notMerged : componentBy(V, leftEnd, rightEnd, F ∪ {e}, w) ≠335          componentBy(V, leftEnd, rightEnd, F ∪ {e}, leftEnd(e))336        rw (componentBy.eq_iff_joined with moreEnds, hw, edgeEnds.left)337        exact Joined.add_edge_apart_iff.backward with338          ends, hw, ⟨notLeft, notRight⟩339      rw ← keep340      exact difference.singleton_membership.backward with341        ⟨(componentsBy.contains with hw), notMerged⟩342    . intro hX343      simp at hX344      obtain ⟨inNew, notMerged⟩ := hX345      obtain ⟨w, hw, rfl⟩ := inNew346      rw (componentBy.eq_iff_joined with moreEnds, hw, edgeEnds.left)347        at notMerged348      obtain ⟨apartLeft, apartRight⟩ :=349        Joined.add_edge_apart_iff.forward with ends, hw, notMerged350      have keep := (componentBy.add_edge_unchanged with351        ends, edgeEnds, apart, hw).backward with ⟨apartLeft, apartRight⟩352      rw ← (componentBy.eq_iff_joined with ends, hw, edgeEnds.left)353        at apartLeft354      rw ← (componentBy.eq_iff_joined with ends, hw, edgeEnds.right)355        at apartRight356      have inOld : componentBy(V, leftEnd, rightEnd, F, w) ∈357          componentsBy(V, leftEnd, rightEnd, F) :=358        componentsBy.contains with hw359      rw keep360      simp361  -- Count: two components removed on one side, one on the other.362  have finiteOld := componentsBy.finite at V, leftEnd, rightEnd, F363    with finiteVertices364  have finiteNew := componentsBy.finite at V, leftEnd, rightEnd, F ∪ {e}365    with finiteVertices366  have finiteInner : Finite(componentsBy(V, leftEnd, rightEnd, F) ∖367      {componentBy(V, leftEnd, rightEnd, F, leftEnd(e))}) :=368    Finite.difference with finiteOld369  have finiteRest : Finite(componentsBy(V, leftEnd, rightEnd, F ∪ {e}) ∖370      {componentBy(V, leftEnd, rightEnd, F ∪ {e}, leftEnd(e))}) :=371    Finite.difference with finiteNew372  have rightInner : componentBy(V, leftEnd, rightEnd, F, rightEnd(e)) ∈373      componentsBy(V, leftEnd, rightEnd, F) ∖374        {componentBy(V, leftEnd, rightEnd, F, leftEnd(e))} :=375    difference.singleton_membership.backward with ⟨rightIn, different⟩376  have removeLeft := cardinality.remove with finiteOld, leftIn377  have removeRight := cardinality.remove with finiteInner, rightInner378  have removeMerged := cardinality.remove with finiteNew, mergedIn379  rw rest at removeRight380  rw [removeMerged, removeLeft, removeRight]381  arith382383-- Along no edges a vertex is joined only to itself, so the components of ∅384-- are the singletons and there are as many as vertices.385theorem Joined.empty (leftEnd rightEnd u v : Set)386  requires joined : Joined(leftEnd, rightEnd, ∅, u, v)387  shows v = u388proof389  have closed : ClosedUnder(leftEnd, rightEnd, ∅, {u}) by simp [ClosedUnder]390  have self : u ∈ {u} by simp391  exact singleton.membership.forward with (joined with {u}, self, closed)392393defgraph componentMap (V leftEnd rightEnd F : Set) (u ∈ V) : 𝒫(V) :=394  componentBy(V, leftEnd, rightEnd, F, u)395proof396  apply powerset.membership_iff.backward397  exact componentBy.subset at V, leftEnd, rightEnd, F, u398399theorem componentMap.image (V leftEnd rightEnd F : Set)400  shows functionImage(componentMap(V, leftEnd, rightEnd, F), V, 𝒫(V)) =401    componentsBy(V, leftEnd, rightEnd, F)402proof403  ext X404  constructor405  . intro hX406    obtain ⟨_, u, hu, rfl⟩ := functionImage.membership.forward with hX407    have value := componentMap.value at V, leftEnd, rightEnd, F, u with hu408    rw value409    exact componentsBy.contains with hu410  . intro hX411    obtain ⟨u, hu, rfl⟩ := hX412    have value := componentMap.value at V, leftEnd, rightEnd, F, u with hu413    have inPowerset : componentBy(V, leftEnd, rightEnd, F, u) ∈ 𝒫(V) :=414      powerset.membership_iff.backward with415        (componentBy.subset at V, leftEnd, rightEnd, F, u)416    symm at value417    exact functionImage.membership.backward with ⟨inPowerset, u, hu, value⟩418419theorem componentsBy.empty_count (V leftEnd rightEnd : Set)420  requires finiteVertices : Finite(V)421  shows cardinality(componentsBy(V, leftEnd, rightEnd, ∅)) = cardinality(V)422proof423  have function := componentMap.function at V, leftEnd, rightEnd, ∅424  have injective :425      InjectiveBetween(componentMap(V, leftEnd, rightEnd, ∅), V, 𝒫(V))426    apply Injective.of_pointwise with function427    intros x hx y hy same428    rw [(componentMap.value at V, leftEnd, rightEnd, ∅, x with hx),429      (componentMap.value at V, leftEnd, rightEnd, ∅, y with hy)] at same430    symm431    exact Joined.empty with (componentBy.joined_of_eq with hy, same)432  have count := cardinality.injective_image with433    injective, Subset.reflexive, finiteVertices434  have image := componentMap.image at V, leftEnd, rightEnd, ∅435  rwa image at count436437-- Each edge merges at most two components: |V| ≤ |F| + |components of F|.438theorem componentsBy.lower_bound (V leftEnd rightEnd F : Set)439  requires finiteVertices : Finite(V)440  requires finite : Finite(F)441  requires ends : ∀ e ∈ F, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V442  shows cardinality(V) ≤443    cardinality(F) + cardinality(componentsBy(V, leftEnd, rightEnd, F))444proof445  induction finite with G e446  | empty =>447    rw [(componentsBy.empty_count with finiteVertices), cardinality.empty]448    arith449  | insert using ih =>450    have GEnds := ends_in.subset with ends, GSubset451    have edgeEnds := ends with e, eMember452    have grown := cardinality.union_singleton with GFinite, eFresh453    by_cases bridged : Joined(leftEnd, rightEnd, G, leftEnd(e), rightEnd(e))454    . have same := componentsBy.add_edge_joined with GEnds, edgeEnds, bridged455      rw same456      arith457    . have count := componentsBy.add_edge_apart with458        finiteVertices, GEnds, edgeEnds, bridged459      arith460461-- Connectivity and the number of components: a disconnected edge set has462-- two components or more, a connected one exactly one.463theorem Connects.witness_apart (V leftEnd rightEnd F : Set)464  requires disconnected : ¬Connects(V, leftEnd, rightEnd, F)465  shows ∃ u ∈ V, ∃ v ∈ V, ¬Joined(leftEnd, rightEnd, F, u, v)466proof467  by_contra none468  apply disconnected469  intros u hu v hv470  by_contra apart471  exact none with ⟨u, hu, v, hv, apart⟩472473theorem componentsBy.two_of_disconnected (V leftEnd rightEnd F : Set)474  requires finiteVertices : Finite(V)475  requires disconnected : ¬Connects(V, leftEnd, rightEnd, F)476  shows 2 ≤ cardinality(componentsBy(V, leftEnd, rightEnd, F))477proof478  obtain ⟨u, hu, v, hv, apart⟩ := Connects.witness_apart with disconnected479  have inU := componentsBy.contains at V, leftEnd, rightEnd, F, u with hu480  have inV := componentsBy.contains at V, leftEnd, rightEnd, F, v with hv481  have finiteComponents := componentsBy.finite at V, leftEnd, rightEnd, F482    with finiteVertices483  have singletonSubset : {componentBy(V, leftEnd, rightEnd, F, u)} ⊆484      componentsBy(V, leftEnd, rightEnd, F) :=485    singleton.subset_iff.backward with inU486  have fresh : ¬componentBy(V, leftEnd, rightEnd, F, v) ∈487      {componentBy(V, leftEnd, rightEnd, F, u)}488    intro member489    have same := singleton.membership.forward with member490    symm at same491    exact apart with (componentBy.joined_of_eq with hv, same)492  have strict := cardinality.strict with493    finiteComponents, singletonSubset, inV, fresh494  rw cardinality.singleton at strict495  arith496497theorem componentBy.eq_vertices (V leftEnd rightEnd F u : Set)498  requires connected : Connects(V, leftEnd, rightEnd, F)499  requires vertex : u ∈ V500  shows componentBy(V, leftEnd, rightEnd, F, u) = V501proof502  ext v503  constructor504  . intro hv505    exact hv.left506  . intro hv507    have joined := connected with u, vertex, v, hv508    exact ⟨hv, joined⟩509510theorem componentsBy.connected_subset (V leftEnd rightEnd F : Set)511  requires connected : Connects(V, leftEnd, rightEnd, F)512  shows componentsBy(V, leftEnd, rightEnd, F) ⊆ {V}513proof514  intros X hX515  obtain ⟨u, hu, rfl⟩ := hX516  have same := componentBy.eq_vertices with connected, hu517  rw same518  simp519520theorem componentsBy.le_one_of_connected (V leftEnd rightEnd F : Set)521  requires connected : Connects(V, leftEnd, rightEnd, F)522  shows cardinality(componentsBy(V, leftEnd, rightEnd, F)) ≤ 1523proof524  have subset := componentsBy.connected_subset with connected525  have bound := cardinality.monotone with subset, Finite.singleton526  rwa cardinality.singleton at bound527528theorem componentsBy.connected_count (V leftEnd rightEnd F : Set)529  requires connected : Connects(V, leftEnd, rightEnd, F)530  requires nonempty : V ≠ ∅531  shows cardinality(componentsBy(V, leftEnd, rightEnd, F)) = 1532proof533  have subset := componentsBy.connected_subset with connected534  obtain ⟨u, hu⟩ := Nonempty.of_ne_empty with nonempty535  have contains := componentsBy.contains at V, leftEnd, rightEnd, F, u with hu536  have same := componentBy.eq_vertices with connected, hu537  rw same at contains538  have reverse : {V} ⊆ componentsBy(V, leftEnd, rightEnd, F) :=539    singleton.subset_iff.backward with contains540  have equal := Subset.antisymmetric with subset, reverse541  rw [equal, cardinality.singleton]542543theorem Graph.ends (V E leftEnd rightEnd : Set)544  requires graph : Graph(V, E, leftEnd, rightEnd)545  shows ∀ e ∈ E, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V546proof547  obtain ⟨leftFunction, rightFunction⟩ := graph548  intros e he549  exact ⟨(FunctionBetween.apply_closed with leftFunction, he),550    (FunctionBetween.apply_closed with rightFunction, he)⟩551552-- In an even edge set the ends of every edge are joined by the other edges:553-- otherwise the edge alone would leave the component of one of its ends,554-- and an even edge set leaves every vertex set an even number of times.555theorem EvenEdgeSet.ends_joined (V leftEnd rightEnd C f : Set)556  requires finiteVertices : Finite(V)557  requires ends : ∀ e ∈ C, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V558  requires even : EvenEdgeSet(V, leftEnd, rightEnd, C)559  requires edge : f ∈ C560  shows Joined(leftEnd, rightEnd, C ∖ {f}, leftEnd(f), rightEnd(f))561proof562  by_contra apart563  have restEnds := ends_in.subset with ends, (difference.subset_left at C, {f})564  have edgeEnds := ends with f, edge565  have closed := componentBy.closed at V, leftEnd, rightEnd, C ∖ {f},566    leftEnd(f) with restEnds567  have subsetV := componentBy.subset at V, leftEnd, rightEnd, C ∖ {f},568    leftEnd(f)569  have leftIn := componentBy.self at V, leftEnd, rightEnd, C ∖ {f}, leftEnd(f)570    with edgeEnds.left571  have rightOut :572      ¬rightEnd(f) ∈ componentBy(V, leftEnd, rightEnd, C ∖ {f}, leftEnd(f))573    intro member574    exact apart with member.right575  have cut : crossing(leftEnd, rightEnd, C,576      componentBy(V, leftEnd, rightEnd, C ∖ {f}, leftEnd(f))) = {f}577    ext g578    rw singleton.membership579    constructor580    . intro hg581      obtain ⟨inC, unbalanced⟩ := crossing.membership.forward with hg582      by_contra other583      have inRest : g ∈ C ∖ {f} by simp584      have balanced := closed with g, inRest585      tauto586    . intro same587      rw same588      apply crossing.membership.backward589      tauto590  exact EvenEdgeSet.crossing_ne_singleton with591    finiteVertices, even, subsetV, cut592593-- A path between the two ends of an edge, together with the edge, is even.594theorem EvenEdgeSet.of_path_edge (V leftEnd rightEnd P e : Set)595  requires finite : Finite(P)596  requires outside : ¬e ∈ P597  requires distinct : leftEnd(e) ≠ rightEnd(e)598  requires path : ∀ w ∈ V, (Even(degreeIn(leftEnd, rightEnd, P, w)) ↔599    (w ≠ leftEnd(e) ∧ w ≠ rightEnd(e)))600  shows EvenEdgeSet(V, leftEnd, rightEnd, P ∪ {e})601proof602  have finiteEdge := Finite.singleton at e603  have apart : Disjoint(P, {e}) by simp [Disjoint.iff]604  constructor605  . exact Finite.union with finite, finiteEdge606  . intros w hw607    have sum := degreeIn.union_disjoint at leftEnd, rightEnd, P, {e}, w608      with finite, finiteEdge, apart609    have parity := path with w, hw610    rw sum611    by_cases atEnd : leftEnd(e) = w ∨ rightEnd(e) = w612    . -- At an end of e the path has odd degree and e supplies one more.613      have one := degreeIn.end with distinct, atEnd614      have odd : ¬Even(degreeIn(leftEnd, rightEnd, P, w))615        intro even616        have away := parity.forward with even617        tauto618      have notOne := Even.not_one619      rw [one, Even.add_iff]620      tauto621    . have notLeft : leftEnd(e) ≠ w by tauto622      have notRight : rightEnd(e) ≠ w by tauto623      have away : w ≠ leftEnd(e) ∧ w ≠ rightEnd(e) by tauto624      have zero := degreeIn.absent with notLeft, notRight625      rw [zero, add.right_unit]626      exact parity.backward with away627