Theorem SimpleGraph.preconnected_iff_reachable_eq_top

Modification history

2026-01-02 14:40
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
feat(Combinatorics/SimpleGraph/Acyclic): characterise maximal acyclic subgraphs (#32043) …
Added SimpleGraph.preconnected_iff_reachable_eq_topView on Github →