Path

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

Statistics

Metric	Count
Definitions `mapPath`, `toPath`, `Path`, `BoundedPaths`, `comp`, `decidableEqBddPathsOfDecidableEq`, `decidableEqBddPathsZero`, `decidableEqBoundedPaths`, `instDecidableEq`, `instInhabited`, `length`, `toList`	12
Theorems `mapPath_comp`, `mapPath_comp_apply`, `mapPath_cons`, `mapPath_id`, `mapPath_nil`, `mapPath_toPath`, `comp_assoc`, `comp_cons`, `comp_inj`, `comp_inj'`, `comp_inj_left`, `comp_inj_right`, `comp_injective_left`, `comp_injective_right`, `comp_nil`, `comp_toPath_eq_cons`, `cons_ne_nil`, `eq_nil_of_length_zero`, `eq_of_length_zero`, `eq_toPath_comp_of_length_eq_succ`, `heq_of_cons_eq_cons`, `hom_heq_of_cons_eq_cons`, `instSubsingletonBddPaths`, `isChain_cons_toList_nonempty`, `isChain_toList_nonempty`, `length_comp`, `length_cons`, `length_ne_zero_iff_eq_comp`, `length_ne_zero_iff_eq_cons`, `length_nil`, `length_toPath`, `nil_comp`, `nil_ne_cons`, `obj_eq_of_cons_eq_cons`, `toList_chain_nonempty`, `toList_comp`, `toList_inj`, `toList_injective`	38
Total	50

Prefunctor

Definitions

Name	Category	Theorems
`mapPath` 📖	CompOp	13 math math: `CategoryTheory.Cat.freeMap_map`, `mapPath_nil`, `mapPath_id`, `CategoryTheory.Localization.Construction.lift_map`, `mapPath_toPath`, `CategoryTheory.Quiv.lift_map`, `CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse_obj_map`, `mapPath_comp`, `pathStar_apply`, `CategoryTheory.Localization.Construction.liftToPathCategory_map`, `mapPath_cons`, `mapPath_comp_apply`, `CategoryTheory.Prefunctor.mapPath_comp'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mapPath_comp` 📖	mathematical	—	`mapPath` `Quiver.Path.comp` `obj`	—	—
`mapPath_comp_apply` 📖	mathematical	—	`mapPath` `comp` `obj`	—	—
`mapPath_cons` 📖	mathematical	—	`mapPath` `Quiver.Path.cons` `obj` `map`	—	—
`mapPath_id` 📖	mathematical	—	`mapPath` `id`	—	—
`mapPath_nil` 📖	mathematical	—	`mapPath` `Quiver.Path.nil` `obj`	—	—
`mapPath_toPath` 📖	mathematical	—	`mapPath` `Quiver.Hom.toPath` `obj` `map`	—	—

Quiver

Definitions

Name	Category	Theorems
`Path` 📖	CompData	23 math math: `SingleObj.pathEquivList_nil`, `Path.heq_of_cons_eq_cons`, `IsFreeGroupoid.path_nonempty_of_hom`, `StronglyConnectedComponent.eq`, `IsStronglyConnected.nonempty_path`, `exists_path_of_stronglyConnectedComponent_eq`, `WeaklyConnectedComponent.eq`, `Path.cast_eq_cast`, `Path.eq_cast_iff_heq`, `Matrix.pow_apply_pos_iff_nonempty_path`, `isStronglyConnected_iff`, `Path.comp_injective_left`, `SingleObj.pathEquivList_symm_cons`, `CategoryTheory.FreeBicategory.preinclusion_map₂`, `Path.comp_injective_right`, `Path.cast_heq`, `RootedConnected.nonempty_path`, `SingleObj.pathEquivList_symm_nil`, `Path.cast_eq_iff_heq`, `SingleObj.pathEquivList_cons`, `stronglyConnectedComponent_singleton_iff`, `StronglyConnectedComponent.mk_eq_mk`, `Path.toList_injective`

Quiver.Hom

Definitions

Name	Category	Theorems
`toPath` 📖	CompOp	16 math math: `Quiver.Path.length_ne_zero_iff_eq_comp`, `Quiver.Path.exists_mem_notMem_hom_path_path_of_notMem_mem`, `Quiver.Path.exists_notMem_mem_hom_path_path_of_notMem_mem`, `SSet.OneTruncation₂.HoRel₂.mk`, `Quiver.Path.vertices_toPath`, `Quiver.Path.vertices_toPath_tail`, `CategoryTheory.Paths.of_map`, `Prefunctor.mapPath_toPath`, `CategoryTheory.Cat.FreeRefl.quotientFunctor_map_id`, `Quiver.Path.eq_toPath_comp_of_length_eq_succ`, `CategoryTheory.composePath_toPath`, `CategoryTheory.Paths.lift_toPath`, `Quiver.Path.length_toPath`, `Quiver.Path.reverse_toPath`, `CategoryTheory.toQuotientPaths_map`, `Quiver.Path.comp_toPath_eq_cons`

Quiver.Path

Definitions

Name	Category	Theorems
`BoundedPaths` 📖	CompOp	1 math math: `instSubsingletonBddPaths`
`comp` 📖	CompOp	32 math math: `length_ne_zero_iff_eq_comp`, `exists_mem_notMem_hom_path_path_of_notMem_mem`, `exists_notMem_mem_hom_path_path_of_notMem_mem`, `exists_eq_comp_and_notMem_tail_of_mem_vertices`, `comp_inj_left`, `toList_comp`, `comp_eq_nil_iff`, `comp_injective_left`, `vertices_comp`, `comp_inj'`, `CategoryTheory.composePath_comp`, `nil_comp`, `reverse_comp`, `comp_injective_right`, `eq_toPath_comp_of_length_eq_succ`, `comp_inj`, `comp_inj_right`, `addWeightOfEPs_comp`, `comp_assoc`, `weight_comp`, `Prefunctor.mapPath_comp`, `exists_eq_comp_of_mem_vertices`, `length_comp`, `comp_nil`, `weightOfEPs_comp`, `exists_eq_comp_and_length_eq_of_lt_length`, `addWeight_comp`, `CategoryTheory.FreeBicategory.normalizeAux_nil_comp`, `comp_toPath_eq_cons`, `exists_eq_comp_of_le_length`, `comp_cons`, `CategoryTheory.Prefunctor.mapPath_comp'`
`decidableEqBddPathsOfDecidableEq` 📖	CompOp	—
`decidableEqBddPathsZero` 📖	CompOp	—
`decidableEqBoundedPaths` 📖	CompOp	—
`instDecidableEq` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`length` 📖	CompOp	17 math math: `length_ne_zero_iff_eq_comp`, `length_cons`, `length_nil`, `nil_of_comp_eq_nil_right`, `comp_eq_nil_iff`, `Matrix.pow_apply_pos_iff_nonempty_path`, `Quiver.IsSStronglyConnected.exists_pos_path`, `Quiver.shortest_path_spec`, `nil_of_comp_eq_nil_left`, `vertices_length`, `length_eq_zero_iff`, `length_comp`, `Quiver.IsSStronglyConnected.exists_pos_cycle`, `exists_eq_comp_and_length_eq_of_lt_length`, `Quiver.StronglyConnectedComponent.IsSStronglyConnected.pos_cycle`, `length_toPath`, `Quiver.isSStronglyConnected_iff`
`toList` 📖	CompOp	6 math math: `toList_comp`, `toList_inj`, `toList_chain_nonempty`, `isChain_toList_nonempty`, `isChain_cons_toList_nonempty`, `toList_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_assoc` 📖	mathematical	—	`comp`	—	`comp_cons`
`comp_cons` 📖	mathematical	—	`comp` `cons`	—	—
`comp_inj` 📖	mathematical	`length`	`comp`	—	`HEq.eq`
`comp_inj'` 📖	mathematical	`length`	`comp`	—	`length_comp`
`comp_inj_left` 📖	mathematical	—	`comp`	—	`comp_injective_left`
`comp_inj_right` 📖	mathematical	—	`comp`	—	`comp_injective_right`
`comp_injective_left` 📖	mathematical	—	`Quiver.Path` `comp`	—	—
`comp_injective_right` 📖	mathematical	—	`Quiver.Path` `comp`	—	`comp_inj'`
`comp_nil` 📖	mathematical	—	`comp` `nil`	—	—
`comp_toPath_eq_cons` 📖	mathematical	—	`comp` `Quiver.Hom.toPath` `cons`	—	—
`cons_ne_nil` 📖	—	—	—	—	—
`eq_nil_of_length_zero` 📖	mathematical	`length`	`nil`	—	—
`eq_of_length_zero` 📖	—	`length`	—	—	—
`eq_toPath_comp_of_length_eq_succ` 📖	mathematical	`length`	`comp` `Quiver.Hom.toPath`	—	`eq_nil_of_length_zero` `eq_of_length_zero` `length_cons`
`heq_of_cons_eq_cons` 📖	mathematical	`cons`	`Quiver.Path`	—	—
`hom_heq_of_cons_eq_cons` 📖	mathematical	`cons`	`Quiver.Hom`	—	—
`instSubsingletonBddPaths` 📖	mathematical	—	`BoundedPaths`	—	—
`isChain_cons_toList_nonempty` 📖	mathematical	—	`Quiver.Hom` `toList`	—	—
`isChain_toList_nonempty` 📖	mathematical	—	`Quiver.Hom` `toList`	—	—
`length_comp` 📖	mathematical	—	`length` `comp`	—	—
`length_cons` 📖	mathematical	—	`length` `cons`	—	—
`length_ne_zero_iff_eq_comp` 📖	mathematical	—	`comp` `Quiver.Hom.toPath` `length`	—	`eq_toPath_comp_of_length_eq_succ`
`length_ne_zero_iff_eq_cons` 📖	mathematical	—	`cons`	—	—
`length_nil` 📖	mathematical	—	`length` `nil`	—	—
`length_toPath` 📖	mathematical	—	`length` `Quiver.Hom.toPath`	—	—
`nil_comp` 📖	mathematical	—	`comp` `nil`	—	`comp_cons`
`nil_ne_cons` 📖	—	—	—	—	—
`obj_eq_of_cons_eq_cons` 📖	—	`cons`	—	—	—
`toList_chain_nonempty` 📖	mathematical	—	`Quiver.Hom` `toList`	—	`isChain_cons_toList_nonempty`
`toList_comp` 📖	mathematical	—	`toList` `comp`	—	—
`toList_inj` 📖	mathematical	`Quiver.Hom`	`toList`	—	`toList_injective`
`toList_injective` 📖	mathematical	`Quiver.Hom`	`Quiver.Path` `toList`	—	—

---

← Back to Index