Documentation

Mathlib.Combinatorics.Quiver.Path.Decomposition

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₂)