Revision #1561 → #2875 · back to history
modifiedEntering equals leaving at non-terminal vertex39a499394d62
| Field | From #1561 | To #2875 |
|---|
| note | `IsTrail.even_countP_edges_iff` states the count of edges at vertex x in a trail is even iff x is not an endpoint, formalizing the entering=leaving property. | `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. |
modifiedEven-degree condition for interior land massesf3026f7a246c
| Field | From #1561 | To #2875 |
|---|
| note | `IsEulerian.even_degree_iff` states Even (G.degree x) ↔ (the walk's endpoints differ → x is neither endpoint), capturing the even-degree condition at non-endpoint vertices. | `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. |
modifiedDegree of a nodee16ade5a3770
| Field | From #1561 | To #2875 |
|---|
| note | `SimpleGraph.degree` is defined as the cardinality of the neighbor finset. | `SimpleGraph.degree` (verified in `Finite.lean` line 201) is defined as the cardinality of the neighbor finset. |
modifiedEuler–Hierholzer characterization of Eulerian trails7e86a7191cb8
| Field | From #1561 | To #2875 |
|---|
| note | Only the necessary direction is in Mathlib (`IsEulerian.card_odd_degree` 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` at line 151 shows 0 or 2 odd-degree vertices); the existence (sufficient) direction is an explicit TODO in `Trails.lean`. |
modifiedEulerian trail1025a76643b8
| Field | From #1561 | To #2875 |
|---|
| note | `SimpleGraph.Walk.IsEulerian` is defined as a walk visiting every edge exactly once. | `SimpleGraph.Walk.IsEulerian` (verified in `Trails.lean` line 79) is defined as a walk visiting every edge exactly once. |
modifiedEulerian circuit5eab888de08e
| Field | From #1561 | To #2875 |
|---|
| note | Mathlib has `IsEulerian` and `IsCircuit` separately; an Eulerian circuit is their conjunction (as noted in the `IsEulerian` docstring) but no dedicated `IsEulerianCircuit` predicate is defined. | Mathlib has `IsEulerian` and `IsCircuit` separately; an Eulerian circuit is their conjunction but no dedicated `IsEulerianCircuit` predicate is defined. |
addedGraph (as vertices and edges)3aa30aac233d
addedGraph equality depends only on incidence9291f29e937f