Theoremresearch
Robertson-Seymour graph minor theorem
Also called Graph minor theorem, Robertson-Seymour theorem, Wagner's conjecture.
Every infinite family of graphs contains a pair where one is a minor of the other; minor-closed families have finite obstruction sets.
Every infinite family of graphs contains a pair where one is a minor of the other; minor-closed families have finite obstruction sets.
About this page
The build computes these levels from the evidence in the repository. Each row says what the next level needs. Read what the levels mean.
| Ladder | Level | What the next level needs |
|---|---|---|
| Human proof | H0 no proof |
|
| Lean | L0 no Lean part |
|
| Visual | V0 none |
|
| Writing | W0 stub |
|
Tag B4ES2D Edit this page History Report an error