WalkDecomp

📁 Source: Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean

Statistics

Metric	Count
Definitions `dropUntil`, `rotate`, `takeUntil`	3
Theorems `count_edges_takeUntil_le_one`, `count_support_takeUntil_eq_one`, `darts_dropUntil_subset`, `darts_takeUntil_subset`, `dropUntil_copy`, `dropUntil_eq_drop`, `dropUntil_first`, `edges_dropUntil_subset`, `edges_takeUntil_subset`, `getVert_le_length_takeUntil_eq_iff`, `getVert_length_takeUntil`, `getVert_lt_length_takeUntil_ne`, `getVert_takeUntil`, `isSubwalk_dropUntil`, `isSubwalk_takeUntil`, `length_dropUntil`, `length_dropUntil_le`, `length_takeUntil`, `length_takeUntil_le`, `length_takeUntil_lt`, `mem_support_iff_exists_append`, `mem_support_iff_exists_getVert`, `mem_support_rotate_iff`, `nil_takeUntil`, `notMem_support_takeUntil_support_takeUntil_subset`, `rotate_darts`, `rotate_edges`, `snd_takeUntil`, `support_dropUntil_subset`, `support_rotate`, `support_takeUntil_subset`, `takeUntil_append_of_mem_left`, `takeUntil_cons`, `takeUntil_copy`, `takeUntil_eq_take`, `takeUntil_first`, `takeUntil_nil`, `takeUntil_takeUntil`, `take_spec`	39
Total	42

SimpleGraph.Walk

Definitions

Name	Category	Theorems
`dropUntil` 📖	CompOp	13 math math: `IsTrail.dropUntil`, `take_spec`, `edges_dropUntil_subset`, `dropUntil_copy`, `support_dropUntil_subset`, `dropUntil_eq_drop`, `length_dropUntil`, `IsPath.dropUntil`, `dropUntil_first`, `IsTrail.disjoint_edges_takeUntil_dropUntil`, `isSubwalk_dropUntil`, `darts_dropUntil_subset`, `length_dropUntil_le`
`rotate` 📖	CompOp	8 math math: `rotate_edges`, `toSubgraph_rotate`, `mem_support_rotate_iff`, `IsTrail.rotate`, `support_rotate`, `IsCycle.rotate`, `IsCircuit.rotate`, `rotate_darts`
`takeUntil` 📖	CompOp	25 math math: `endpoint_notMem_support_takeUntil`, `snd_takeUntil`, `length_takeUntil_lt`, `length_takeUntil_le`, `support_takeUntil_subset`, `take_spec`, `edges_takeUntil_subset`, `takeUntil_copy`, `takeUntil_first`, `takeUntil_eq_take`, `count_support_takeUntil_eq_one`, `isSubwalk_takeUntil`, `takeUntil_nil`, `IsTrail.takeUntil`, `exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty`, `length_takeUntil`, `takeUntil_append_of_mem_left`, `count_edges_takeUntil_le_one`, `takeUntil_cons`, `nil_takeUntil`, `IsTrail.disjoint_edges_takeUntil_dropUntil`, `IsPath.takeUntil`, `darts_takeUntil_subset`, `IsCycle.isPath_takeUntil`, `getVert_length_takeUntil`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`count_edges_takeUntil_le_one` 📖	mathematical	`support`	`Sym2` `Sym2.instDecidableEq` `edges` `takeUntil`	—	`takeUntil_first` `mem_support_nil_iff` `edges_cons` `zero_add`
`count_support_takeUntil_eq_one` 📖	mathematical	`support`	`takeUntil`	—	`takeUntil_first` `List.count_eq_one_of_mem` `mem_support_nil_iff`
`darts_dropUntil_subset` 📖	mathematical	`support`	`SimpleGraph.Dart` `darts` `dropUntil`	—	`take_spec` `darts_append`
`darts_takeUntil_subset` 📖	mathematical	`support`	`SimpleGraph.Dart` `darts` `takeUntil`	—	`take_spec` `darts_append`
`dropUntil_copy` 📖	mathematical	`support` `copy`	`dropUntil`	—	—
`dropUntil_eq_drop` 📖	mathematical	`support`	`dropUntil` `copy` `getVert` `drop` `getVert_support_idxOf`	—	`ext_support` `getVert_support_idxOf` `support_copy` `dropUntil_first` `drop_support_eq_support_drop_min` `inf_of_le_left` `getVert_cons` `drop_cons_eq` `dropUntil.eq_2`
`dropUntil_first` 📖	mathematical	`support`	`dropUntil`	—	`dropUntil.eq_def`
`edges_dropUntil_subset` 📖	mathematical	`support`	`Sym2` `edges` `dropUntil`	—	`darts_dropUntil_subset`
`edges_takeUntil_subset` 📖	mathematical	`support`	`Sym2` `edges` `takeUntil`	—	`darts_takeUntil_subset`
`getVert_le_length_takeUntil_eq_iff` 📖	mathematical	`support` `length` `takeUntil`	`getVert`	—	—
`getVert_length_takeUntil` 📖	mathematical	`support`	`getVert` `length` `takeUntil`	—	`take_spec`
`getVert_lt_length_takeUntil_ne` 📖	—	`support` `length` `takeUntil`	—	—	`length_support` `LT.lt.le` `getVert_eq_support_getElem` `getVert_takeUntil` `count_support_takeUntil_eq_one` `support_eq_concat`
`getVert_takeUntil` 📖	mathematical	`support` `length` `takeUntil`	`getVert`	—	`take_spec` `getVert_append` `LE.le.lt_or_eq` `getVert_length` `getVert_zero`
`isSubwalk_dropUntil` 📖	mathematical	`support`	`IsSubwalk` `dropUntil`	—	`take_spec` `append_nil`
`isSubwalk_takeUntil` 📖	mathematical	`support`	`IsSubwalk` `takeUntil`	—	`take_spec`
`length_dropUntil` 📖	mathematical	`support`	`length` `dropUntil`	—	`getVert_support_idxOf` `dropUntil_eq_drop` `length_copy` `drop_length`
`length_dropUntil_le` 📖	mathematical	`support`	`length` `dropUntil`	—	`take_spec` `add_comm` `length_append`
`length_takeUntil` 📖	mathematical	`support`	`length` `takeUntil`	—	`getVert_support_idxOf` `takeUntil_eq_take` `length_copy` `take_length` `inf_of_le_left`
`length_takeUntil_le` 📖	mathematical	`support`	`length` `takeUntil`	—	`take_spec` `length_append`
`length_takeUntil_lt` 📖	mathematical	`support`	`length` `takeUntil`	—	`LE.le.lt_iff_ne` `length_takeUntil_le` `getVert_length` `getVert_takeUntil` `le_refl`
`mem_support_iff_exists_append` 📖	mathematical	—	`support` `append`	—	`take_spec`
`mem_support_iff_exists_getVert` 📖	mathematical	—	`support` `getVert` `length`	—	`getVert_length_takeUntil` `length_takeUntil_le` `getVert_mem_support`
`mem_support_rotate_iff` 📖	mathematical	`support`	`rotate`	—	—
`nil_takeUntil` 📖	mathematical	`support`	`Nil` `takeUntil`	—	`Nil.eq` `takeUntil_first`
`notMem_support_takeUntil_support_takeUntil_subset` 📖	mathematical	`support` `takeUntil`	`support_takeUntil_subset`	—	`support_takeUntil_subset` `takeUntil_takeUntil` `length_takeUntil_lt` `takeUntil.congr_simp`
`rotate_darts` 📖	mathematical	`support`	`List.IsRotated` `SimpleGraph.Dart` `darts` `rotate`	—	`darts_append` `List.IsRotated.trans` `List.isRotated_append` `take_spec` `List.IsRotated.refl`
`rotate_edges` 📖	mathematical	`support`	`List.IsRotated` `Sym2` `edges` `rotate`	—	`List.IsRotated.map` `rotate_darts`
`snd_takeUntil` 📖	mathematical	`support`	`snd` `takeUntil`	—	`getVert_takeUntil`
`support_dropUntil_subset` 📖	mathematical	`support`	`dropUntil`	—	`take_spec` `mem_support_append_iff`
`support_rotate` 📖	mathematical	`support`	`List.IsRotated` `rotate`	—	`tail_support_append` `List.IsRotated.trans` `List.isRotated_append` `take_spec` `List.IsRotated.refl`
`support_takeUntil_subset` 📖	mathematical	`support`	`takeUntil`	—	`take_spec` `mem_support_append_iff`
`takeUntil_append_of_mem_left` 📖	mathematical	`support`	`takeUntil` `append` `subset_support_append_left`	—	`subset_support_append_left` `takeUntil_first` `mem_support_nil_iff` `support_cons` `takeUntil_cons`
`takeUntil_cons` 📖	mathematical	`support` `SimpleGraph.Adj`	`takeUntil` `cons`	—	—
`takeUntil_copy` 📖	mathematical	`support` `copy`	`takeUntil`	—	—
`takeUntil_eq_take` 📖	mathematical	`support`	`takeUntil` `copy` `getVert` `take` `getVert_support_idxOf`	—	`ext_support` `getVert_support_idxOf` `support_copy` `getVert_cons` `take_cons_eq` `takeUntil_cons` `support_cons`
`takeUntil_first` 📖	mathematical	—	`takeUntil` `start_mem_support` `nil`	—	`start_mem_support`
`takeUntil_nil` 📖	mathematical	`support` `nil`	`takeUntil`	—	—
`takeUntil_takeUntil` 📖	mathematical	`support` `takeUntil`	`support_takeUntil_subset`	—	`support_takeUntil_subset` `subset_support_append_left` `takeUntil_append_of_mem_left` `take_spec` `takeUntil.congr_simp`
`take_spec` 📖	mathematical	`support`	`append` `takeUntil` `dropUntil`	—	`mem_support_nil_iff` `cons.congr_simp`

---

← Back to Index