Theorems · Theorem · combinatorics
SimpleGraph.Walk.edges_subset_edgeSet
∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) ⦃e : Sym2 V⦄, e ∈ p.edges → e ∈ G.edgeSetEvery edge in a walk's edge list is an edge of the graph.
It is written in this form (rather than using ⊆) to avoid unsightly coercions.
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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.Walkstatement and proof · cited by 915
- Sym2statement and proof · cited by 737
- SimpleGraph.edgeSetstatement · cited by 199
- SimpleGraph.Walk.edgesstatement and proof · cited by 145
- SimpleGraph.Walk.brecOnproof · cited by 15
Cited by11
Results whose statement or proof uses this declaration.
- SimpleGraph.Walk.adj_of_mem_edgesproof · cited by 4
- SimpleGraph.Walk.IsEulerian.isTrailproof · cited by 4
- SimpleGraph.isAcyclic_iff_forall_isBridgeproof · cited by 4
- SimpleGraph.reachable_deleteEdges_iff_exists_walkproof · cited by 3
- SimpleGraph.Walk.IsEulerian.mem_edges_iffproof · cited by 2
- SimpleGraph.Walk.IsTrail.length_le_card_edgeFinsetproof · cited by 2
- SimpleGraph.Walk.transfer_selfstatement and proof · cited by 1
- SimpleGraph.IsBridge.sup_edge_of_not_reachable_of_isBridgeproof · cited by 1
- SimpleGraph.Walk.IsTrail.isEulerian_iffproof · cited by 1
- SimpleGraph.IsBridge.notMem_edges_of_isCycleproof · cited by 1
- SimpleGraph.Walk.map_toDeleteEdges_eqproof · cited by 0