Decomposition

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

Statistics

Metric	Count
Definitions	0
Theorems exists_mem_notMem_hom_path_path_of_notMem_mem, exists_notMem_mem_hom_path_path_of_notMem_mem	2
Total	2

Quiver.Path

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mem_notMem_hom_path_path_of_notMem_mem 📖	mathematical	Set Set.instMembership	comp Quiver.Hom.toPath	—	exists_notMem_mem_hom_path_path_of_notMem_mem
exists_notMem_mem_hom_path_path_of_notMem_mem 📖	mathematical	Set Set.instMembership	comp Quiver.Hom.toPath	—	eq_of_length_zero IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd length_ne_zero_iff_eq_cons LT.lt.ne'

---

← Back to Index