Theorem SimpleGraph.reachable_fromEdgeSet_eq_reflTransGen_toRel

Modification history

2025-12-09 05:22

Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

feat(Combinatorics/SimpleGraph/Connectivity/Connected): a few lemmas about `Reachable` (#30570)

Added SimpleGraph.reachable_fromEdgeSet_eq_reflTransGen_toRel View on Github →