Theorem SimpleGraph.reachable_fromEdgeSet_fromRel_eq_reflTransGen

Modification history

2026-06-10 08:59

Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean

chore(Order/Defs/Unbundled): deprecate `def Symmetric` in favor of `class Std.Symm` (#38092)

Modified SimpleGraph.reachable_fromEdgeSet_fromRel_eq_reflTransGen View on Github →

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_fromRel_eq_reflTransGen View on Github →