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

4.3 \(\bar\omega (\mathrm{AC}_n - v) = 2\) for every \(v\)

Theorem 4.3 omegabar_AC_del
✓
#

Uses

Rocq declarations

Theorem omegabar_AC_del (v : ACm) :
  (3 <= m)%N -> ω̄(del_tournament v) = 2.

Source: theories/applications/k5/acn_base.v:423

Decoded. Deleting any single vertex \(v\) from \(\mathrm{AC}_n\) drops the invariant to \(2\).

Theorem 4.5 AC_vertex_transitive
✓
#

Uses

Rocq declarations

Lemma AC_vertex_transitive : vertex_transitiveb AC.

Source: theories/constructions/circulant.v:134