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

6.6 \(\bar\omega = 1\) exactly for transitive tournaments

Theorem 6.7 omegabar_transb
✓
#

Uses

Rocq declarations

Lemma omegabar_transb : 0 < #|T| -> (ω̄(T) == 1) = transb T.

Source: theories/invariants/omegabar.v:74

Decoded. For a nonempty tournament, \(\bar\omega (T) = 1\) iff \(T\) is transitive (2.6) — the sanity anchor for reading \(\bar\omega \) as a distance from transitivity. (The statement is a Boolean equation between \(\bar\omega (T) = 1\) and transb T, both Booleans.)