Subwalks

📁 Source: Mathlib/Combinatorics/SimpleGraph/Walks/Subwalks.lean

Statistics

Metric	Count
Definitions `IsSubwalk`	1
Theorems `concat`, `cons`, `copy`, `darts_isInfix`, `darts_subset`, `dropLast`, `edges_isInfix`, `edges_subset`, `map`, `support_subset`, `tail`, `trans`, `drop_isSubwalk_drop`, `infix_support_iff_mem_edges`, `isSubwalk_antisymm`, `isSubwalk_concat`, `isSubwalk_cons`, `isSubwalk_drop`, `isSubwalk_iff_darts_isInfix`, `isSubwalk_iff_support_isInfix`, `isSubwalk_nil_iff`, `isSubwalk_nil_iff_mem_support`, `isSubwalk_of_append_left`, `isSubwalk_of_append_right`, `isSubwalk_rfl`, `isSubwalk_take`, `isSubwalk_toWalk_adj_iff_mem_darts`, `isSubwalk_toWalk_iff_mem_darts`, `isSubwalk_toWalk_iff_mem_edges`, `length_le_of_isSubwalk`, `nil_isSubwalk`, `nil_isSubwalk_iff_exists`, `take_isSubwalk_take`	33
Total	34

SimpleGraph.Walk

Definitions

Name	Category	Theorems
`IsSubwalk` 📖	MathDef	20 math math: `isSubwalk_of_append_right`, `drop_isSubwalk_drop`, `isSubwalk_concat`, `isSubwalk_toWalk_iff_mem_darts`, `isSubwalk_nil_iff_mem_support`, `isSubwalk_drop`, `isSubwalk_take`, `isSubwalk_rfl`, `isSubwalk_takeUntil`, `isSubwalk_iff_darts_isInfix`, `nil_isSubwalk`, `isSubwalk_toWalk_iff_mem_edges`, `take_isSubwalk_take`, `isSubwalk_nil_iff`, `isSubwalk_of_append_left`, `isSubwalk_iff_support_isInfix`, `isSubwalk_dropUntil`, `nil_isSubwalk_iff_exists`, `isSubwalk_cons`, `isSubwalk_toWalk_adj_iff_mem_darts`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`drop_isSubwalk_drop` 📖	mathematical	—	`IsSubwalk` `getVert` `drop`	—	`Nat.le_induction` `isSubwalk_rfl` `IsSubwalk.trans` `getVert_zero` `IsSubwalk.tail` `IsSubwalk.copy` `drop_zero`
`infix_support_iff_mem_edges` 📖	mathematical	—	`support` `Sym2` `edges`	—	`adj_of_infix_support` `SimpleGraph.Adj.symm` `isSubwalk_toWalk_iff_mem_edges` `adj_of_mem_edges`
`isSubwalk_antisymm` 📖	—	`IsSubwalk`	—	—	`ext_support` `List.infix_antisymm` `isSubwalk_iff_support_isInfix`
`isSubwalk_concat` 📖	mathematical	`SimpleGraph.Adj`	`IsSubwalk` `concat`	—	`IsSubwalk.concat` `isSubwalk_rfl`
`isSubwalk_cons` 📖	mathematical	`SimpleGraph.Adj`	`IsSubwalk` `cons`	—	`IsSubwalk.cons` `isSubwalk_rfl`
`isSubwalk_drop` 📖	mathematical	—	`IsSubwalk` `getVert` `drop`	—	`append_take_drop_eq` `append_nil`
`isSubwalk_iff_darts_isInfix` 📖	mathematical	`Nil`	`IsSubwalk` `SimpleGraph.Dart` `darts`	—	`isSubwalk_iff_support_isInfix` `SimpleGraph.Dart.ext`
`isSubwalk_iff_support_isInfix` 📖	mathematical	—	`IsSubwalk` `support`	—	`length_support` `getVert_eq_support_getElem` `head_support` `le_rfl` `getVert_length` `ext_support` `support_append` `support_copy` `take_support_eq_support_take_succ` `drop_support_eq_support_drop_min` `support_eq_cons`
`isSubwalk_nil_iff` 📖	mathematical	—	`IsSubwalk` `nil` `copy`	—	—
`isSubwalk_nil_iff_mem_support` 📖	mathematical	—	`IsSubwalk` `nil` `support`	—	`isSubwalk_iff_support_isInfix` `List.singleton_infix_iff`
`isSubwalk_of_append_left` 📖	mathematical	`append`	`IsSubwalk`	—	—
`isSubwalk_of_append_right` 📖	mathematical	`append`	`IsSubwalk`	—	`append_nil`
`isSubwalk_rfl` 📖	mathematical	—	`IsSubwalk`	—	`append_nil`
`isSubwalk_take` 📖	mathematical	—	`IsSubwalk` `getVert` `take`	—	`append_take_drop_eq`
`isSubwalk_toWalk_adj_iff_mem_darts` 📖	mathematical	—	`IsSubwalk` `SimpleGraph.Dart.toProd` `SimpleGraph.Adj.toWalk` `SimpleGraph.Dart.adj` `SimpleGraph.Dart` `darts`	—	`isSubwalk_toWalk_iff_mem_darts` `SimpleGraph.Dart.adj`
`isSubwalk_toWalk_iff_mem_darts` 📖	mathematical	`SimpleGraph.Adj`	`IsSubwalk` `SimpleGraph.Adj.toWalk` `SimpleGraph.Dart` `darts`	—	—
`isSubwalk_toWalk_iff_mem_edges` 📖	mathematical	`SimpleGraph.Adj`	`IsSubwalk` `SimpleGraph.Adj.toWalk` `SimpleGraph.Adj.symm` `Sym2` `edges`	—	`SimpleGraph.Adj.symm` `isSubwalk_toWalk_iff_mem_darts` `edges.eq_1` `SimpleGraph.Dart.adj` `Sym2.rel_iff'` `Sym2.eq` `SimpleGraph.Dart.edge.eq_1`
`length_le_of_isSubwalk` 📖	mathematical	`IsSubwalk`	`length`	—	—
`nil_isSubwalk` 📖	mathematical	—	`IsSubwalk` `nil`	—	`append_nil`
`nil_isSubwalk_iff_exists` 📖	mathematical	—	`IsSubwalk` `nil` `append`	—	`append_nil`
`take_isSubwalk_take` 📖	mathematical	—	`IsSubwalk` `getVert` `take`	—	`Nat.le_induction` `isSubwalk_rfl` `IsSubwalk.trans` `isSubwalk_take` `isSubwalk_of_append_left` `take_support_eq_support_take_succ` `length_support`

SimpleGraph.Walk.IsSubwalk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`concat` 📖	mathematical	`SimpleGraph.Walk.IsSubwalk` `SimpleGraph.Adj`	`SimpleGraph.Walk.concat`	—	`SimpleGraph.Walk.append_concat`
`cons` 📖	mathematical	`SimpleGraph.Walk.IsSubwalk` `SimpleGraph.Adj`	`SimpleGraph.Walk.cons`	—	—
`copy` 📖	mathematical	`SimpleGraph.Walk.IsSubwalk`	`SimpleGraph.Walk.copy`	—	`SimpleGraph.Walk.support_copy` `SimpleGraph.Walk.isSubwalk_iff_support_isInfix`
`darts_isInfix` 📖	mathematical	`SimpleGraph.Walk.IsSubwalk`	`SimpleGraph.Dart` `SimpleGraph.Walk.darts`	—	—
`darts_subset` 📖	mathematical	`SimpleGraph.Walk.IsSubwalk`	`SimpleGraph.Dart` `SimpleGraph.Walk.darts`	—	`darts_isInfix`
`dropLast` 📖	mathematical	`SimpleGraph.Walk.IsSubwalk`	`SimpleGraph.Walk.penultimate` `SimpleGraph.Walk.dropLast`	—	`trans` `SimpleGraph.Walk.isSubwalk_take`
`edges_isInfix` 📖	mathematical	`SimpleGraph.Walk.IsSubwalk`	`Sym2` `SimpleGraph.Walk.edges`	—	—
`edges_subset` 📖	mathematical	`SimpleGraph.Walk.IsSubwalk`	`Sym2` `SimpleGraph.Walk.edges`	—	`edges_isInfix`
`map` 📖	mathematical	`SimpleGraph.Walk.IsSubwalk`	`DFunLike.coe` `SimpleGraph.Hom` `RelHom.instFunLike` `SimpleGraph.Adj` `SimpleGraph.Walk.map`	—	`SimpleGraph.Walk.support_map` `SimpleGraph.Walk.isSubwalk_iff_support_isInfix`
`support_subset` 📖	mathematical	`SimpleGraph.Walk.IsSubwalk`	`SimpleGraph.Walk.support`	—	`SimpleGraph.Walk.isSubwalk_iff_support_isInfix`
`tail` 📖	mathematical	`SimpleGraph.Walk.IsSubwalk`	`SimpleGraph.Walk.snd` `SimpleGraph.Walk.tail`	—	`trans` `SimpleGraph.Walk.isSubwalk_drop`
`trans` 📖	—	`SimpleGraph.Walk.IsSubwalk`	—	—	`SimpleGraph.Walk.append_assoc`

---

← Back to Index