Traversal

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

Statistics

Metric	Count
Definitions `firstDart`, `getVert`, `lastDart`, `penultimate`, `snd`	5
Theorems `adj_getVert_succ`, `adj_of_infix_support`, `adj_penultimate`, `adj_snd`, `darts_getElem_eq_getVert`, `edge_firstDart`, `edge_lastDart`, `firstDart_eq`, `firstDart_eq_head_darts`, `firstDart_mem_darts`, `firstDart_toProd`, `getLast_darts_eq_lastDart`, `getLast_darts_snd`, `getLast_edges_eq_mk_penultimate_end`, `getVert_comp_val_eq_get_support`, `getVert_cons`, `getVert_cons_succ`, `getVert_eq_getD_support`, `getVert_eq_support_getElem`, `getVert_eq_support_getElem?`, `getVert_length`, `getVert_mem_support`, `getVert_nil`, `getVert_of_length_le`, `getVert_support_idxOf`, `getVert_zero`, `head_darts_eq_firstDart`, `head_darts_fst`, `head_edges_eq_mk_start_snd`, `lastDart_eq`, `lastDart_eq_getLast_darts`, `lastDart_mem_darts`, `lastDart_toProd`, `mk_penultimate_end_eq_getLast_edges`, `mk_penultimate_end_mem_edges`, `mk_start_snd_eq_head_edges`, `mk_start_snd_mem_edges`, `penultimate_cons_cons`, `penultimate_cons_nil`, `penultimate_cons_of_not_nil`, `penultimate_mem_dropLast_support`, `penultimate_nil`, `range_getVert_eq_range_support_getElem`, `snd_cons`, `snd_eq_support_getElem_one`, `snd_mem_tail_support`, `support_getElem_eq_getVert`, `support_getElem_length_sub_one_eq_penultimate`, `support_getElem_one`	49
Total	54

SimpleGraph.Walk

Definitions

Name	Category	Theorems
`firstDart` 📖	CompOp	6 math math: `firstDart_eq_head_darts`, `firstDart_mem_darts`, `firstDart_toProd`, `edge_firstDart`, `firstDart_eq`, `head_darts_eq_firstDart`
`getVert` 📖	CompOp	72 math math: `nil_take_iff`, `IsHamiltonian.getVertEquiv_apply`, `edges_take`, `darts_take`, `IsPath.ncard_neighborSet_toSubgraph_internal_eq_two`, `getVert_eq_support_getElem?`, `toSubgraph_adj_iff`, `range_getVert_eq_range_support_getElem`, `take_zero`, `IsHamiltonian.getVert_surjective`, `getVert_cons`, `drop_zero`, `nil_drop_of_length_le`, `getVert_reverse`, `getVert_le_length_takeUntil_eq_iff`, `drop_isSubwalk_drop`, `getVert_tail`, `getVert_support_idxOf`, `getVert_zero`, `getVert_append`, `tail_cons_eq`, `getVert_takeUntil`, `IsPath.getVert_eq_start_iff`, `isSubwalk_drop`, `IsPath.neighborSet_toSubgraph_internal`, `getVert_mem_support`, `getVert_of_length_le`, `append_take_drop_eq`, `IsCycle.getVert_endpoint_iff`, `getVert_mem_tail_support`, `IsPath.getVert_injOn`, `take_of_length_le`, `darts_drop`, `getVert_eq_support_getElem`, `darts_getElem_eq_getVert`, `nil_drop_iff`, `tail_cons`, `take_length`, `drop_add_heq`, `isSubwalk_take`, `getVert_cons_succ`, `getVert_comp_val_eq_get_support`, `getVert_copy`, `adj_getVert_succ`, `IsPath.getVert_injOn_iff`, `dropUntil_eq_drop`, `takeUntil_eq_take`, `take_add_heq`, `drop_getVert`, `drop_length`, `getVert_length`, `take_isSubwalk_take`, `support_getElem_eq_getVert`, `edges_drop`, `getVert_nil`, `drop_add_eq`, `IsCycle.getVert_injOn'`, `drop_of_length_le`, `IsPath.getVert_eq_end_iff`, `toSubgraph_adj_getVert`, `take_cons_eq`, `take_getVert`, `take_add_eq`, `drop_cons_eq`, `getVert_eq_getD_support`, `drop_support_eq_support_drop_min`, `getVert_map`, `IsCycle.neighborSet_toSubgraph_internal`, `mem_support_iff_exists_getVert`, `IsCycle.getVert_injOn`, `getVert_length_takeUntil`, `take_support_eq_support_take_succ`
`lastDart` 📖	CompOp	6 math math: `lastDart_eq_getLast_darts`, `lastDart_toProd`, `edge_lastDart`, `lastDart_eq`, `getLast_darts_eq_lastDart`, `lastDart_mem_darts`
`penultimate` 📖	CompOp	23 math math: `penultimate_mem_dropLast_support`, `penultimate_nil`, `adj_penultimate`, `penultimate_concat`, `penultimate_reverse`, `lastDart_toProd`, `toSubgraph_adj_penultimate`, `edge_lastDart`, `IsCycle.neighborSet_toSubgraph_endpoint`, `penultimate_cons_of_not_nil`, `dropLast_cons_of_not_nil`, `IsPath.eq_penultimate_of_mem_edges`, `mk_penultimate_end_eq_getLast_edges`, `dropLast_cons_cons`, `penultimate_cons_cons`, `snd_reverse`, `mk_penultimate_end_mem_edges`, `support_getElem_length_sub_one_eq_penultimate`, `penultimate_cons_nil`, `dropLast_concat`, `getLast_edges_eq_mk_penultimate_end`, `IsSubwalk.dropLast`, `IsPath.neighborSet_toSubgraph_endpoint`
`snd` 📖	CompOp	37 math math: `IsPath.eq_snd_of_mem_edges`, `snd_takeUntil`, `IsPath.snd_of_toSubgraph_adj`, `length_tail_add_one`, `tail_nil`, `head_edges_eq_mk_start_snd`, `penultimate_reverse`, `IsHamiltonianCycle.isHamiltonian_tail`, `isHamiltonianCycle_isCycle_and_isHamiltonian_tail`, `getVert_tail`, `mk_start_snd_eq_head_edges`, `snd_cons`, `tail_cons_nil`, `SimpleGraph.IsCycles.snd_of_mem_support_of_isPath_of_adj`, `IsPath.neighborSet_toSubgraph_startpoint`, `IsCycle.neighborSet_toSubgraph_endpoint`, `isCycle_iff_isPath_tail_and_le_length`, `Nil.tail`, `firstDart_toProd`, `edge_firstDart`, `snd_eq_support_getElem_one`, `IsPath.disjoint_support_of_append`, `toSubgraph_adj_snd`, `snd_mem_tail_support`, `snd_reverse`, `support_tail`, `support_tail_of_not_nil`, `IsCycle.exists_isCycle_snd_verts_eq`, `IsPath.tail`, `cons_support_tail`, `support_getElem_one`, `SimpleGraph.walkLengthTwoEquivCommonNeighbors_apply_coe`, `mk_start_snd_mem_edges`, `adj_snd`, `IsSubwalk.tail`, `cons_tail_eq`, `IsCycle.isPath_tail`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`adj_getVert_succ` 📖	mathematical	`length`	`SimpleGraph.Adj` `getVert`	—	`getVert_zero`
`adj_of_infix_support` 📖	mathematical	`support`	`SimpleGraph.Adj`	—	`adj_getVert_succ` `getVert_eq_support_getElem?`
`adj_penultimate` 📖	mathematical	`Nil`	`SimpleGraph.Adj` `penultimate`	—	`getVert_length` `nil_iff_length_eq` `adj_getVert_succ`
`adj_snd` 📖	mathematical	`Nil`	`SimpleGraph.Adj` `snd`	—	`getVert_zero` `zero_add` `adj_getVert_succ`
`darts_getElem_eq_getVert` 📖	mathematical	`SimpleGraph.Dart` `darts`	`getVert` `adj_getVert_succ` `length` `length_darts`	—	`SimpleGraph.Dart.ext` `adj_getVert_succ` `length_darts` `le_of_lt` `length_support` `fst_darts_getElem` `getVert_eq_support_getElem` `snd_darts_getElem`
`edge_firstDart` 📖	mathematical	`Nil`	`SimpleGraph.Dart.edge` `firstDart` `snd`	—	—
`edge_lastDart` 📖	mathematical	`Nil`	`SimpleGraph.Dart.edge` `lastDart` `penultimate`	—	—
`firstDart_eq` 📖	mathematical	`Nil` `SimpleGraph.Dart` `darts`	`firstDart`	—	`adj_getVert_succ` `length_darts` `getVert_zero` `zero_add` `darts_getElem_eq_getVert`
`firstDart_eq_head_darts` 📖	mathematical	`Nil`	`firstDart` `SimpleGraph.Dart` `darts` `Iff.not` `darts_eq_nil`	—	`Iff.not` `darts_eq_nil` `head_darts_eq_firstDart`
`firstDart_mem_darts` 📖	mathematical	`Nil`	`SimpleGraph.Dart` `darts` `firstDart`	—	`Iff.not` `darts_eq_nil` `firstDart_eq_head_darts`
`firstDart_toProd` 📖	mathematical	`Nil`	`SimpleGraph.Dart.toProd` `firstDart` `snd`	—	—
`getLast_darts_eq_lastDart` 📖	mathematical	—	`SimpleGraph.Dart` `darts` `lastDart` `Nil` `Iff.not` `darts_eq_nil`	—	—
`getLast_darts_snd` 📖	mathematical	—	`SimpleGraph.Dart.toProd` `SimpleGraph.Dart` `darts`	—	`Iff.not` `darts_eq_nil` `getLast_darts_eq_lastDart`
`getLast_edges_eq_mk_penultimate_end` 📖	mathematical	—	`Sym2` `edges` `penultimate`	—	`Iff.not` `darts_eq_nil` `getLast_darts_eq_lastDart`
`getVert_comp_val_eq_get_support` 📖	mathematical	—	`support` `getVert`	—	—
`getVert_cons` 📖	mathematical	`SimpleGraph.Adj`	`getVert` `cons`	—	`getVert_cons_succ`
`getVert_cons_succ` 📖	mathematical	`SimpleGraph.Adj`	`getVert` `cons`	—	—
`getVert_eq_getD_support` 📖	mathematical	—	`getVert` `support`	—	`getVert_eq_support_getElem?`
`getVert_eq_support_getElem` 📖	mathematical	`length`	`getVert` `support` `length_support`	—	—
`getVert_eq_support_getElem?` 📖	mathematical	`length`	`getVert` `support`	—	`length_support` `getVert_eq_support_getElem`
`getVert_length` 📖	mathematical	—	`getVert` `length`	—	`getVert_of_length_le` `Eq.le`
`getVert_mem_support` 📖	mathematical	—	`support` `getVert`	—	`getVert_zero`
`getVert_nil` 📖	mathematical	—	`getVert` `nil`	—	—
`getVert_of_length_le` 📖	mathematical	`length`	`getVert`	—	—
`getVert_support_idxOf` 📖	mathematical	`support`	`getVert`	—	—
`getVert_zero` 📖	mathematical	—	`getVert`	—	—
`head_darts_eq_firstDart` 📖	mathematical	—	`SimpleGraph.Dart` `darts` `firstDart` `Nil` `Iff.not` `darts_eq_nil`	—	—
`head_darts_fst` 📖	mathematical	—	`SimpleGraph.Dart.toProd` `SimpleGraph.Dart` `darts`	—	`Iff.not` `darts_eq_nil` `head_darts_eq_firstDart`
`head_edges_eq_mk_start_snd` 📖	mathematical	—	`Sym2` `edges` `snd`	—	`Iff.not` `darts_eq_nil` `head_darts_eq_firstDart`
`lastDart_eq` 📖	mathematical	`Nil` `SimpleGraph.Dart` `darts`	`lastDart`	—	`adj_getVert_succ` `length_darts` `getVert_of_length_le` `darts_getElem_eq_getVert`
`lastDart_eq_getLast_darts` 📖	mathematical	`Nil`	`lastDart` `SimpleGraph.Dart` `darts` `Iff.not` `darts_eq_nil`	—	—
`lastDart_mem_darts` 📖	mathematical	`Nil`	`SimpleGraph.Dart` `darts` `lastDart`	—	`Iff.not` `darts_eq_nil` `lastDart_eq_getLast_darts`
`lastDart_toProd` 📖	mathematical	`Nil`	`SimpleGraph.Dart.toProd` `lastDart` `penultimate`	—	—
`mk_penultimate_end_eq_getLast_edges` 📖	mathematical	`Nil`	`penultimate` `Sym2` `edges` `Iff.not` `edges_eq_nil`	—	`Iff.not` `edges_eq_nil` `getLast_edges_eq_mk_penultimate_end`
`mk_penultimate_end_mem_edges` 📖	mathematical	`Nil`	`Sym2` `edges` `penultimate`	—	`Iff.not` `edges_eq_nil` `mk_penultimate_end_eq_getLast_edges`
`mk_start_snd_eq_head_edges` 📖	mathematical	`Nil`	`snd` `Sym2` `edges` `Iff.not` `edges_eq_nil`	—	`Iff.not` `edges_eq_nil` `head_edges_eq_mk_start_snd`
`mk_start_snd_mem_edges` 📖	mathematical	`Nil`	`Sym2` `edges` `snd`	—	`Iff.not` `edges_eq_nil` `mk_start_snd_eq_head_edges`
`penultimate_cons_cons` 📖	mathematical	`SimpleGraph.Adj`	`penultimate` `cons`	—	—
`penultimate_cons_nil` 📖	mathematical	`SimpleGraph.Adj`	`penultimate` `cons` `nil`	—	—
`penultimate_cons_of_not_nil` 📖	mathematical	`SimpleGraph.Adj` `Nil`	`penultimate` `cons`	—	—
`penultimate_mem_dropLast_support` 📖	mathematical	`Nil`	`support` `penultimate`	—	`SimpleGraph.Adj.ne` `adj_penultimate`
`penultimate_nil` 📖	mathematical	—	`penultimate` `nil`	—	—
`range_getVert_eq_range_support_getElem` 📖	mathematical	—	`Set.range` `getVert` `support`	—	`Set.ext`
`snd_cons` 📖	mathematical	`SimpleGraph.Adj`	`snd` `cons`	—	`getVert_zero`
`snd_eq_support_getElem_one` 📖	mathematical	`Nil`	`snd` `support`	—	`support_getElem_one`
`snd_mem_tail_support` 📖	mathematical	`Nil`	`support` `snd`	—	`getVert_zero`
`support_getElem_eq_getVert` 📖	mathematical	`support`	`getVert`	—	`length_support` `getVert_eq_support_getElem`
`support_getElem_length_sub_one_eq_penultimate` 📖	mathematical	—	`support` `length` `penultimate`	—	—
`support_getElem_one` 📖	mathematical	`support`	`snd`	—	—

---

← Back to Index