B&M’s general isomorphism needs two bijections, one on vertices and one on edges, respecting incidence. For simple graphs the edge bijection carries no information — at most one edge joins any pair — so an adjacency-preserving vertex bijection already induces it. This is precisely why Mathlib can define \(G \)≃\(g H\) as an equivalence of vertex types with G.Adj u v \(\leftrightarrow \) H.Adj (\(\theta \) u) (\(\theta \) v), and this exercise is the justification for using it throughout the file.

Exercise 1.1.3 gives \(\varepsilon \le C(\nu ,2)\); equality means the injection from edges to pairs is onto, i.e. every pair carries an edge — the definition of complete.

"Complete" is \(G = \top \), the top of the lattice of simple graphs on \(V\).

\(K_{m,n}\) contains exactly one edge for each choice of a vertex in \(X\) and one in \(Y\), so edges biject with \(X \times Y\).

The carrier is Fin m \(\oplus \) Fin n, so "opposite sides" is a Sum case split; step 1’s well-definedness is the only fiddly point.

\(mn\) with fixed sum \(\nu \) is largest when the parts are equal, giving \(\nu ^{2}/4\); the bound is attained by \(K_{\nu /2,\nu /2}\).

Stated in the cleared form \(4\varepsilon \le \nu ^{2}\) to stay in \(\mathbb {N}\), and bipartiteness as Colorable 2 — Mathlib’s IsBipartite is an abbreviation for exactly that.

Every vertex has degree \(k\), one neighbour per coordinate flip.

! \(k - 1\) is \(\mathbb {N}\)-subtraction; the \(k = 0\) case is where it bites, and it happens to come out right, but only by accident of \(0 * _= 0\).

Split the tuples by the parity of their number of \(1\)s; an edge flips exactly one entry and so changes that parity, making every edge cross between the classes.

Bipartiteness as Colorable 2, with ZMod 2 as the palette and simpa bridging to Fin 2.

Self-complementary means \(G \cong G^{c}\), so \(G\) has exactly half of all possible edges — which forces \(\nu \equiv 0\) or 1 (mod 4). The smallest examples are the path \(P_{4}\) (\(\nu = 4\)) and the cycle \(C_{5}\) (\(\nu = 5\)).

\(G[V']\) keeps \(V'\) and all edges of \(G\) with both ends there. If \(G\) is complete, every pair inside \(V'\) is joined and every such edge is retained — so \(G[V']\) is complete.

Every edge of \(H\) is an edge of \(G\), so the very same bipartition still has every edge crossing: deleting vertices and edges can never create an edge inside a part.

Stated for \(H \le G\) on the same carrier, which is the spanning-subgraph case. B&M’s "subgraph" also allows dropping vertices; that case is induce_bipartite and the two together are subgraph_induce_bipartite, both below.

subgraph_bipartite covers B&M’s spanning subgraphs (same vertex set, fewer edges); this covers the other half of what B&M call a subgraph — throwing vertices away. Restricting a bipartition to a vertex subset still leaves every surviving edge crossing.

This is the exercise as the book states it; subgraph_bipartite (edges only) and induce_bipartite (vertices only) are the two halves, and either alone is what a Lean transcription tends to produce. ! Nothing in the proof uses \(2\) specifically; the identical two lines give the Colorable k statement for any \(k\), should a general version be wanted.

Adding up the degrees counts each edge twice, once from each end. The name comes from the reading: if each edge is a handshake, the total hands shaken is twice the number of handshakes. Loops are consistent, contributing \(2\) to their single end.

A sum of odd numbers is even precisely when there is an even number of terms. This tiny corollary is what §1.9 uses to derive Sperner’s lemma, and through it Brouwer’s fixed-point theorem — the chapter’s most striking application.

\(2\varepsilon /\nu \) is the average degree, since the degrees sum to \(2\varepsilon \) and there are \(\nu \) of them; an average lies between the extremes.

Stated multiplicatively to avoid division: \(\nu \cdot \delta \le 2\varepsilon \le \nu \cdot \Delta \). [Nonempty V] keeps minDegree/maxDegree meaningful — both are sInf/sSup-like and degenerate on an empty carrier.

Count the edges twice, once from each side. ! \(hk : 0 \lt k\) is essential — a \(0\)-regular graph has no edges and its two parts can have any sizes.

IsBipartiteWith s t is Mathlib’s explicit-bipartition form, stronger than Colorable 2 and what step 1 needs. Set.ncard rather than Finset.card, so no decidability on \(s\), \(t\) is required.

Split the vertices in two and keep only the crossing edges — automatically bipartite and spanning — choosing the split to maximise crossings. Then no vertex can have more than half its edges inside its own part, or moving it would improve the split.

Conclusion in the cleared form \(d_G(v) \le 2 d_H(v)\) to stay in \(\mathbb {N}\). ! Step 3’s \(i - c \le 0\) must be argued in \(\mathbb {Z}\) or by Nat.le_of_add_le_add, not by \(\mathbb {N}\)-subtraction.

Two edges are adjacent in the edge graph exactly when they share an end; simplicity makes that end unique, so the count localises at each vertex.

! Step 1’s uniqueness is where simplicity is spent — with parallel edges two edges could share both ends and be counted twice. Part (b) of the exercise, not stated here, notes the edge graph of \(K_{5}\) is the complement of the Petersen graph.

A longest path cannot be extended, so its endpoint’s neighbours are all already on it, forcing it to be long. ! Simplicity is what makes the \(\delta \) neighbours \(\delta \) distinct vertices — and SimpleGraph supplies it for free.

Connectivity is exactly the statement that \(V\) admits no non-trivial cut with no edges across it.

The partition is a set \(s\) with its complement, both required nonempty — equivalent to B&M’s \((V_{1}, V_{2})\).

A disconnected simple graph is sparsest-constrained in the most lopsided split. The bound is sharp: part (b), not stated here, asks for a disconnected simple graph with exactly \(C(\nu -1,2)\) edges — \(K_{\nu -1}\) plus one isolated vertex.

Every pair is joined in \(G^{c}\) by a path of length at most \(2\), so \(G^{c}\) is connected — indeed of diameter \(\le 2\). Equivalently: at least one of \(G\), \(G^{c}\) is always connected.

! Steps 2–3 need \(u \ne w\) and \(v \ne w\), which follow from them being in different components; and "different components" must be extracted from \(\lnot \) Connected — Preconnected failing gives an unreachable pair.

If \(H \le K\) then \(\omega (K) \le \omega (H)\) — adding edges can only merge components.

Not a book statement. This is the general lemma that exercise 1.6.8(a) below is the single-edge instance of, and it is extracted here because Trees.lean’s skeleton for corollary 2.7 asks for it by name: *"the monotonicity \(H \le K \to \omega (K) \le \omega (H)\) is used here and is worth a standalone lemma — chapter 1’s exercise 1.6.8(a) needs the same fact."* Both call sites are served by this one declaration.

Stated with Nat.card, matching Trees.numComponents, so that no DecidableEq on the quotient is needed. ! Exercise 1.6.8(a) below uses Fintype.card; over a Fintype carrier the two agree by Nat.card_eq_fintype_card, but the transfer must be written explicitly at the call site.

Deleting an edge only destroys connections, never creates them; and it affects only the component containing \(e\), which can break into at most the parts reachable from each end. An edge whose deletion does raise the count is a cut edge, the subject of §2.3. ! Part (b), not stated here, notes the analogue fails for vertex deletion — removing one vertex can create many components.

A graph and its complement cannot both be "spread out": if \(G\) is very stretched, \(G^{c}\) must be very compact.

! G.diam is \(\mathbb {N}\)-valued and Mathlib returns \(0\) for a disconnected graph, so 3 < G.diam silently carries "\(G\) is connected" — worth making explicit before relying on step 1.

A connected non-complete graph always contains an induced path on three vertices — adjacency is transitive only when the graph is a disjoint union of complete graphs. * Consumed by Brooks’ theorem 8.4, whose 3-connected case opens by invoking exactly this.

Odd cycles are the sole obstruction to \(2\)-colourability — the fact that makes chapter 8 turn on odd cycles throughout.

Bipartiteness as G.Colorable 2; Mathlib’s two_colorable_iff_forall_loop_even is an equivalent loop-based form and may close this more directly than the cycle form.

A closed trail may revisit vertices, so it need not be a cycle; the claim is that it can be pared down to one through any chosen edge. ! The analogous statement for walks is false — a walk may traverse the same edge back and forth with no cycle present — which is why ht : c.IsTrail (distinct edges) is a hypothesis and not decoration.

hpos : 0 < c.length excludes the trivial closed walk, for which \(he\) would be unsatisfiable anyway but which would otherwise complicate step 1.

If every vertex offers a second way out you can never get stuck, so walking forward must eventually revisit a vertex, and the first revisit closes a cycle. * Contrapositively, an acyclic graph always has a vertex of degree \(\le \) 1 — used repeatedly in chapter 2’s theory of trees, and by chapter 12’s lemma 12.2.1.

Sharpens exercise 1.7.2 from "some cycle exists" to a length bound: a graph in which every vertex has many neighbours cannot consist only of short cycles. * This is chapter 10’s exercise 10.1.7 one dimension down — the directed version bounds directed cycles by max{\(\delta ^{-}\),\(\delta ^{+}\)} + 1 and is used inside Ghouila-Houri’s theorem 10.4.

! B&M add that, up to isomorphism, there is exactly one such graph on \(2k\) vertices, namely \(K_{k,k}\); only the counting half is stated here, and the uniqueness half would be a substantially harder separate result.

Graphs attaining this bound with diameter two are the Moore graphs of exercise 1.7.5; Hoffman and Singleton showed they exist only for \(k = 2, 3, 7\) and possibly \(57\). The case \(k = 3\) is the Petersen graph — the same graph chapter 9 uses as its counterexample to Tait’s approach.

! \(k - 1\) is \(\mathbb {N}\)-subtraction; \(k = 0\) makes the statement \(1 \le \nu \) and girth = 5 unsatisfiable, so the degenerate case is vacuous — but check it rather than assume it.

Each edge added to a forest either joins two different components — possible at most \(\nu - 1\) times — or joins two already-connected vertices, immediately closing a cycle. ! Part (b), due to Pósa and not stated here, strengthens this: \(\varepsilon \ge \nu + 4\) forces two edge-disjoint cycles.

+ Hypothesis repaired. Step 2 needs \(\omega \ge 1\), i.e. Nonempty V. Without it the statement is false on an empty carrier, where \(\nu = \varepsilon = 0\) so \(h\) holds vacuously while no cycle exists (indeed no vertex \(v\) exists to base one at). [Nonempty V] has been added; it is not in B&M only because the book’s graphs are nonempty by convention.