Path Decomposition and Boundary Crossing

This section provides lemmas for decomposing non-empty paths and for reasoning about paths that cross the boundary of a given set of vertices S.

theorem Quiver.Path.exists_notMem_mem_hom_path_path_of_notMem_mem {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) (S : Set V) (ha_not_in_S : a ∉ S) (hb_in_S : b ∈ S) : ∃ u ∉ S, ∃ v ∈ S, ∃ (e : u ⟶ v) (p₁ : Path a u) (p₂ : Path v b), p = p₁.comp (e.toPath.comp p₂)

A path from a vertex not in S to a vertex in S must cross the boundary.

theorem Quiver.Path.exists_mem_notMem_hom_path_path_of_notMem_mem {V : Type u_1} [Quiver V] {a b : V} (p : Path a b) (S : Set V) (ha_in_S : a ∈ S) (hb_not_in_S : b ∉ S) : ∃ u ∈ S, ∃ v ∉ S, ∃ (e : u ⟶ v) (p₁ : Path a u) (p₂ : Path v b), p = p₁.comp (e.toPath.comp p₂)