WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Graph minor

Revision #2903 → #3358 · back to history

modifiedWagner's theorem (planarity)4bd130217d84
FieldFrom #2903To #3358
notePlanar graphs are not defined in Mathlib (only mentioned as a TODO in `SimpleGraph/Coloring/Vertex.lean`), so Wagner's planarity theorem is absent.Planarity is not defined in Mathlib (grep for SimpleGraph planar returns nothing), so Wagner's planarity theorem is absent.
addedEquivalent WQO statement: finitely many minor-minimal elements8b3aa71d127f