Monochromatic independence and infinite outward paths

Two notions are introduced, both for a digraph $D$ on a set $V$ of vertices whose arcs are coloured with values in $\{0,1,2\}$.

Monochromatic independence. A set $S$ of vertices is monochromatically independent when no two distinct vertices $x, y \in S$ are connected by a monochromatic directed path in either direction: there is neither a directed path from $x$ to $y$ nor one from $y$ to $x$ all of whose arcs carry one common colour. This is the notion of independence used by Sands, Sauer and Woodrow (J. Combin. Theory Ser. B 33 (1982), 271–275, p. 271). It is weaker than graph independence — it forbids monochromatic paths, not arcs — but in a tournament every two distinct vertices are joined by an arc, so a tournament's monochromatically independent sets have at most one element. That is why the tournament corollary of the same paper concludes with a single vertex.

No monochromatic infinite outward path. A digraph has no monochromatic infinite outward path when there is no colour $k$ and no injective sequence $x_0, x_1, x_2, \dots$ of vertices such that every consecutive arc $x_n \to x_{n+1}$ has colour $k$. Injectivity is what makes the sequence a path rather than a walk: in the source a path has pairwise distinct vertices. This is the hypothesis of the paper's Theorem 1; it is vacuous when the vertex set is finite.

Formalization Note. Both notions are stated for an arbitrary vertex type and refer to the platform definitions Digraph, ArcColoring and MonochromaticallyReaches, the last being reachability along arcs of a single colour.