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 : V), ¬u ∈ S ∧ ∃ (v : V), 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 : V), u ∈ S ∧ ∃ (v : V), ¬v ∈ S ∧ ∃ (e : u ⟶ v), ∃ (p₁ : Path a u), ∃ (p₂ : Path v b), p = p₁.comp (e.toPath.comp p₂)