Commit 2026-02-13 23:15 265f65e6

View on Github →

feat(Combinatorics/SimpleGraph/Acyclic): every graph has a spanning forest (#33118) We show that every graph has a spanning forest: defined to be an acyclic subgraph with the same reachability relation as the larger graph. As a special case, every connected graph has a spanning tree.

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

modified theorem SimpleGraph.Connected.exists_isTree_le

added theorem SimpleGraph.Connected.exists_isTree_le_of_le_of_isAcyclic

added theorem SimpleGraph.exists_isAcyclic_reachable_eq_le

added theorem SimpleGraph.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic