Revision #1273 → #2254 · back to history
modifiedGraph minore040838337d7
| Field | From #1273 | To #2254 |
|---|
| note | Graph minors are not formalized (explicitly flagged as future work in Combinatorics/Graph/Basic.lean); only the analogous matroid minor relation exists. | Graph minors are not formalized in Mathlib; only the analogous matroid minor relation `Matroid.IsMinor` exists. |
modifiedWagner's theorem (planarity)4bd130217d84
| Field | From #1273 | To #2254 |
|---|
| note | Planar graphs are not defined in Mathlib (listed as a TODO), so this characterization is absent. | Planar graphs are not defined in Mathlib (only mentioned as a TODO in `SimpleGraph/Coloring/Vertex.lean`), so Wagner's planarity theorem is absent. |
modifiedEdge contractiond2f63c264ff2
| Field | From #1273 | To #2254 |
|---|
| note | Graph edge contraction is not defined; the analogous matroid contraction operation `Matroid.contract` (／) exists instead. | Graph edge contraction is not defined; only the analogous matroid contraction operation `Matroid.contract` exists. |
modifiedOrder independence of contractions and deletionscabb628d6ed5
| Field | From #1273 | To #2254 |
|---|
| note | Order-independence of contractions/deletions is proven for matroids (`contract_delete_comm`, `contract_comm`, `contract_delete_contract_delete`), but not for graphs. | Order-independence of contractions/deletions is proven for matroids, but the graph version is not formalized. |
modifiedMinor-monotone function4d1e5b473b3d
| Field | From #1273 | To #2254 |
|---|
| anchor.snippet | is referred to as | A function f is referred to as "minor-monotone" |
| provenance | ai | ai-moderated |
modifiedMinor relation is a partial orderc24b2dc5de2b
| Field | From #1273 | To #2254 |
|---|
| note | A `PartialOrder` instance for the minor order exists for matroids (refl/trans/antisymm lemmas), but not for graphs. | Reflexivity/transitivity/antisymmetry of the minor order exist for matroids, but not for graphs. |
addedHadwiger conjecture proven for k ≤ 6d985d87e3e5c