Commit 2026-03-01 13:37 e5686e7a

View on Github →

feat(Combinatorics/SimpleGraph/Acyclic): acyclic and bridge theorems + golfing (#30640)

Estimated changes

Modified Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

added theorem SimpleGraph.IsAcyclic.isAcyclic_sup_fromEdgeSet_of_not_reachable

added theorem SimpleGraph.isAcyclic_sup_fromEdgeSet_iff

added theorem SimpleGraph.isTree_iff_maximal_isAcyclic

modified theorem SimpleGraph.maximal_isAcyclic_iff_reachable_eq

Modified Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

added theorem SimpleGraph.IsBridge.sup_fromEdgeSet_of_not_reachable

added theorem SimpleGraph.IsBridge.sup_fromEdgeSet_of_not_reachable_of_isBridge