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

4.5 \(\bar\omega (\mathrm{AC}_n[C_3]) = 4\)

Theorem 4.7 omegabar_T4
✓
#

Uses

Rocq declarations

Theorem omegabar_T4 : ω̄(T4) = 4.

Source: theories/applications/k4/k4_value.v:511

Decoded. Here T4 abbreviates the substitution \(\mathrm{AC}_n[C_3]\) (2.19). For every odd \(n = 2m{+}1 \ge 7\), its tournament clique number is exactly \(4\).