Email Gateway (Aug 22 2022 at 15:09): Email Gateway (Aug 22 2022 at 15:09):From: Tobias Nipkow <nipkow@in.tum.de>
Menger's Theorem
Christoph Dittmann
We present a formalization of Menger's Theorem for directed and undirected
graphs in Isabelle/HOL. This well-known result shows that if two non-adjacent
distinct vertices u, v in a directed graph have no separator smaller than n,
then there exist n internally vertex-disjoint paths from u to v. The version for
undirected graphs follows immediately because undirected graphs are a special
case of directed graphs.
https://www.isa-afp.org/entries/Menger.shtml
A theorem with a name - enjoy!
smime.p7s
Last updated: Nov 21 2024 at 12:39 UTC