Theorems · Theorem · combinatorics
SimpleGraph.adj_and_reachable_delete_edges_iff_exists_cycle
∀ {V : Type u} {G : SimpleGraph V} {v w : V},
G.Adj v w ∧ (G.deleteEdges {s(v, w)}).Reachable v w ↔ ∃ u p, p.IsCycle ∧ s(v, w) ∈ p.edges- Cited by
- 3 results in Mathlib
- Foundations
- Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites30
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- SimpleGraphstatement and proof · cited by 3,072
- SimpleGraph.Adjstatement and proof · cited by 1,346
- SimpleGraph.Walkstatement and proof · cited by 915
- Sym2statement and proof · cited by 737
- Sym2.mkstatement and proof · cited by 332
- SimpleGraph.Walk.supportproof · cited by 307
- SimpleGraph.Walk.edgesstatement and proof · cited by 145
- SimpleGraph.Reachablestatement · cited by 141
- SimpleGraph.Walk.IsCyclestatement and proof · cited by 91
- SimpleGraph.Adj.symmproof · cited by 66
- SimpleGraph.deleteEdgesstatement · cited by 64
Cited by3
Results whose statement or proof uses this declaration.
- SimpleGraph.IsBridge.sup_edge_of_not_reachable_of_isBridgeproof · cited by 1
- SimpleGraph.exists_isCycle_of_two_le_isEdgeReachableproof · cited by 1