Commit 2025-12-09 05:22 66eafa53

View on Github →

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

Estimated changes

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

added theorem SimpleGraph.Reachable.mono'

added theorem SimpleGraph.adj_le_reachable

added theorem SimpleGraph.reachable_eq_reflTransGen

added theorem SimpleGraph.reachable_fromEdgeSet_eq_reflTransGen_toRel

added theorem SimpleGraph.reachable_fromEdgeSet_fromRel_eq_reflTransGen