Vertices

📁 Source: Mathlib/Combinatorics/Quiver/Path/Vertices.lean

Statistics

Metric	Count
Definitions `end`, `vertices`	2
Theorems `comp_eq_nil_iff`, `dropLast_append_end_eq`, `end_cons`, `end_mem_vertices`, `exists_eq_comp_and_length_eq_of_lt_length`, `exists_eq_comp_and_notMem_tail_of_mem_vertices`, `exists_eq_comp_of_le_length`, `exists_eq_comp_of_mem_vertices`, `getElem_vertices_zero`, `length_eq_zero_iff`, `length_vertices_pos`, `mem_vertices_cons`, `nil_of_comp_eq_nil_left`, `nil_of_comp_eq_nil_right`, `start_mem_vertices`, `verticesSet_nil`, `vertices_comp`, `vertices_comp_get_length_eq`, `vertices_cons`, `vertices_getLast`, `vertices_head?`, `vertices_head_eq`, `vertices_length`, `vertices_ne_nil`, `vertices_nil`, `vertices_toPath`, `vertices_toPath_tail`	27
Total	29

Quiver.Path

Definitions

Name	Category	Theorems
`end` 📖	CompOp	1 math math: `end_cons`
`vertices` 📖	CompOp	19 math math: `dropLast_append_end_eq`, `length_vertices_pos`, `exists_eq_comp_and_notMem_tail_of_mem_vertices`, `getElem_vertices_zero`, `end_mem_vertices`, `vertices_cons`, `start_mem_vertices`, `vertices_head_eq`, `vertices_head?`, `vertices_toPath`, `vertices_toPath_tail`, `vertices_comp`, `vertices_length`, `vertices_getLast`, `exists_eq_comp_and_length_eq_of_lt_length`, `mem_vertices_cons`, `vertices_nil`, `verticesSet_nil`, `vertices_comp_get_length_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_eq_nil_iff` 📖	mathematical	—	`comp` `nil` `length`	—	`nil_of_comp_eq_nil_left` `nil_of_comp_eq_nil_right` `nil_comp` `length_eq_zero_iff`
`dropLast_append_end_eq` 📖	mathematical	—	`vertices`	—	`vertices_ne_nil` `vertices_getLast`
`end_cons` 📖	mathematical	—	`end` `cons`	—	—
`end_mem_vertices` 📖	mathematical	—	`vertices`	—	`vertices_ne_nil` `vertices_getLast`
`exists_eq_comp_and_length_eq_of_lt_length` 📖	mathematical	`vertices`	`Quiver.Path` `comp` `length` `vertices`	—	`vertices_length` `exists_eq_comp_of_le_length` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `instReflLe` `vertices_comp` `getElem_vertices_zero`
`exists_eq_comp_and_notMem_tail_of_mem_vertices` 📖	mathematical	`vertices`	`Quiver.Path` `comp` `vertices`	—	`mem_vertices_cons`
`exists_eq_comp_of_le_length` 📖	mathematical	`length`	`Quiver.Path` `comp` `length`	—	`Nat.instCanonicallyOrderedAdd` `length_cons`
`exists_eq_comp_of_mem_vertices` 📖	mathematical	`vertices`	`Quiver.Path` `comp`	—	`List.exists_mem_iff_getElem` `exists_eq_comp_and_length_eq_of_lt_length`
`getElem_vertices_zero` 📖	mathematical	—	`vertices`	—	`vertices_length` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Nat.instCanonicallyOrderedAdd`
`length_eq_zero_iff` 📖	mathematical	—	`length` `nil`	—	—
`length_vertices_pos` 📖	mathematical	—	`vertices`	—	`vertices_length` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Nat.instCanonicallyOrderedAdd`
`mem_vertices_cons` 📖	mathematical	—	`vertices` `cons`	—	—
`nil_of_comp_eq_nil_left` 📖	mathematical	`comp` `nil`	`length`	—	`length_comp`
`nil_of_comp_eq_nil_right` 📖	mathematical	`comp` `nil`	`length`	—	`length_comp`
`start_mem_vertices` 📖	mathematical	—	`vertices`	—	—
`verticesSet_nil` 📖	mathematical	—	`setOf` `vertices` `nil` `Set` `Set.instSingletonSet`	—	`Set.mem_setOf`
`vertices_comp` 📖	mathematical	—	`vertices` `comp`	—	`dropLast_append_end_eq`
`vertices_comp_get_length_eq` 📖	mathematical	`length` `vertices` `comp`	`vertices` `comp` `length`	—	`vertices_length` `add_tsub_cancel_right` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `instReflLe` `vertices_comp` `getElem_vertices_zero`
`vertices_cons` 📖	mathematical	—	`vertices` `cons`	—	—
`vertices_getLast` 📖	mathematical	`vertices` `vertices_ne_nil`	`vertices`	—	—
`vertices_head?` 📖	mathematical	—	`vertices`	—	—
`vertices_head_eq` 📖	mathematical	`vertices` `vertices_ne_nil`	`vertices`	—	`vertices_ne_nil`
`vertices_length` 📖	mathematical	—	`vertices` `length`	—	`zero_add`
`vertices_ne_nil` 📖	—	—	—	—	`vertices_length` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Nat.instCanonicallyOrderedAdd`
`vertices_nil` 📖	mathematical	—	`vertices` `nil`	—	—
`vertices_toPath` 📖	mathematical	—	`vertices` `Quiver.Hom.toPath`	—	—
`vertices_toPath_tail` 📖	mathematical	—	`vertices` `Quiver.Hom.toPath`	—	`vertices_toPath`

---

← Back to Index