Tournaments, \(\bar\omega \)-criticality, and directed paths
The formal statements of the digraph-theory library, for mathematicians

4.6 \(\bar\omega (\mathrm{AC}_n[C_3] - v) = 3\) for every \(v\)

Theorem 4.8 omegabar_T4_del
✓
#

Uses

Rocq declarations

Theorem omegabar_T4_del (v : T4) : ω̄(del_tournament v) = 3.

Source: theories/applications/k4/k4_main.v:51

Decoded. Deleting any vertex of \(\mathrm{AC}_n[C_3]\) drops the invariant to \(3\) (by vertex-transitivity all deletions are isomorphic, so this is one computation plus symmetry — see 6.2).