6.2 Vertex-transitive tournaments: one deletion decides criticality
Theorem vt_kcritical (k : nat) (v0 : T) : vertex_transitiveb (T : diGraphType) -> kcritical k T = (ω̄(T) == k) && (ω̄(del_tournament v0) == k.-1).
Source: theories/invariants_advanced/transitive.v:57
Decoded. In a vertex-transitive tournament all single-vertex deletions have the same \(\bar\omega \) (second statement), so \(k\)-criticality reduces to the value of \(\bar\omega (T)\) and of one deletion \(\bar\omega (T - v_0)\) (first statement, a Boolean equivalence).
Theorem omegabar_del_vt : vertex_transitiveb (T : diGraphType) -> forall u v : T, ω̄(del_tournament u) = ω̄(del_tournament v).