OAI/Combinatorics/Sensitivity/Tournament.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Finite tournaments and the target-constant labeling condition.

  1. structure OAI.Paper320.Tournament line 16
  2. structure OAI.Paper320.RegularTournament line 20
  3. structure OAI.Paper320.GoodLabeling line 23
  4. theorem OAI.Paper320.Tournament.ne_of_adj line 31
  5. theorem OAI.Paper320.Tournament.not_adj_reverse line 35
  6. theorem OAI.Paper320.Tournament.adj_or_reverse line 38
  7. theorem OAI.Paper320.Tournament.internal_sink_unique line 43
  8. theorem OAI.Paper320.GoodLabeling.good_implies_card_lt_sixteen line 56