Revision #2875 → #3333 · back to history
modifiedEntering equals leaving at non-terminal vertex39a499394d62
| Field | From #2875 | To #3333 |
|---|
| note | `IsTrail.even_countP_edges_iff` (verified in `Trails.lean` line 54) states the count of edges at vertex x in a trail is even iff x is not a unique endpoint, formalizing the entering=leaving property. | `IsTrail.even_countP_edges_iff` (verified via decl_exists in `Mathlib.Combinatorics.SimpleGraph.Trails`) captures parity of edge-incidences at non-endpoint vertices along a trail. |
modifiedEven-degree condition for interior land massesf3026f7a246c
| Field | From #2875 | To #3333 |
|---|
| note | `IsEulerian.even_degree_iff` (verified in `Trails.lean` line 127) states Even (G.degree x) ↔ (u ≠ v → x ≠ u ∧ x ≠ v), capturing the even-degree condition at non-endpoint vertices. | `IsEulerian.even_degree_iff` (verified via decl_exists) states Even (G.degree x) ↔ (u ≠ v → x ≠ u ∧ x ≠ v), capturing the even-degree condition at non-endpoint vertices. |
modifiedDegree of a nodee16ade5a3770
| Field | From #2875 | To #3333 |
|---|
| note | `SimpleGraph.degree` (verified in `Finite.lean` line 201) is defined as the cardinality of the neighbor finset. | `SimpleGraph.degree` (verified via decl_exists in `Mathlib.Combinatorics.SimpleGraph.Finite`) is the cardinality of the neighbor finset. |
modifiedEuler–Hierholzer characterization of Eulerian trails7e86a7191cb8
| Field | From #2875 | To #3333 |
|---|
| note | Only the necessary direction is in Mathlib (`IsEulerian.card_odd_degree` at line 151 shows 0 or 2 odd-degree vertices); the existence (sufficient) direction is an explicit TODO in `Trails.lean`. | Only the necessary direction is in Mathlib (`IsEulerian.card_odd_degree` gives 0 or 2 odd-degree vertices); the sufficient (existence) direction is a known TODO in `Trails.lean`. |
modifiedEulerian trail1025a76643b8
| Field | From #2875 | To #3333 |
|---|
| note | `SimpleGraph.Walk.IsEulerian` (verified in `Trails.lean` line 79) is defined as a walk visiting every edge exactly once. | `SimpleGraph.Walk.IsEulerian` (verified via decl_exists) is a walk visiting every edge exactly once. |
modifiedEndpoints of an Eulerian path with odd-degree nodesc896b129f55b
| Field | From #2875 | To #3333 |
|---|
| note | The contrapositive of `IsEulerian.even_degree_iff` says odd-degree vertices must be endpoints of the Eulerian walk. | The contrapositive of `IsEulerian.even_degree_iff` says odd-degree vertices must coincide with the endpoints of the Eulerian walk. |
modifiedGraph (as vertices and edges)3aa30aac233d
| Field | From #2875 | To #3333 |
|---|
| note | Mathlib's `SimpleGraph` (verified in `Basic.lean` line 93) formalizes the general abstract graph structure (vertices plus symmetric adjacency); the Königsberg setting is a multigraph, which Mathlib does not directly capture. | Mathlib's `SimpleGraph` (verified via decl_exists) formalizes the general abstract graph (vertices with symmetric adjacency); the Königsberg setting is a multigraph, not directly captured. |
modifiedGraph equality depends only on incidence9291f29e937f
| Field | From #2875 | To #3333 |
|---|
| note | `SimpleGraph.ext` (auto-generated from the `@[ext]` on the `SimpleGraph` structure in `Basic.lean` line 92) shows a simple graph is determined by its adjacency relation. | `SimpleGraph.ext` (verified via decl_exists) shows a simple graph is determined by its adjacency relation. |
addedWalk in a graphb9e0c4e867b4
addedConnected graph403c3c7889e5