Theorems · Theorem · combinatorics
SimpleGraph.Walk.isSubwalk_iff_support_isInfix
∀ {V : Type u_1} {G : SimpleGraph V} {v w v' w' : V} {p₁ : G.Walk v w} {p₂ : G.Walk v' w'},
p₁.IsSubwalk p₂ ↔ p₁.support <:+: p₂.support- Cited by
- 7 results in Mathlib
- Foundations
- Depth 69 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- SimpleGraphstatement and proof · cited by 3,072
- le_rflproof · cited by 1,558
- SimpleGraph.Walkstatement and proof · cited by 915
- SimpleGraph.Walk.supportstatement and proof · cited by 307
- SimpleGraph.Walk.lengthproof · cited by 212
- SimpleGraph.Walk.appendproof · cited by 95
- SimpleGraph.Walk.copyproof · cited by 56
- SimpleGraph.Walk.IsSubwalkstatement and proof · cited by 46
- SimpleGraph.Walk.dropproof · cited by 30
- SimpleGraph.Walk.takeproof · cited by 27
- SimpleGraph.Walk.support_copyproof · cited by 16
- SimpleGraph.Walk.length_supportproof · cited by 15
Cited by7
Results whose statement or proof uses this declaration.
- SimpleGraph.Walk.IsSubwalk.support_subsetproof · cited by 1
- SimpleGraph.Walk.IsPath.exists_isCycle_sublist_of_neproof · cited by 1
- SimpleGraph.Walk.IsSubwalk.copyproof · cited by 1
- SimpleGraph.Walk.isSubwalk_iff_darts_isInfixproof · cited by 0
- SimpleGraph.Walk.isSubwalk_nil_iff_mem_supportproof · cited by 0
- SimpleGraph.Walk.IsSubwalk.mapproof · cited by 0
- SimpleGraph.Walk.isSubwalk_antisymmproof · cited by 0