OAI/Combinatorics/Ramsey/CycleClique/Construction/PathSystemCounts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Elementary counting properties of nontrivial expanded chains.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.chain_clique_count_two line 13
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.chains_length_le_assignedCount line 32
  3. theorem OAI.CycleClique.Construction.ExpandedPathSystem.amount_eq_zero_of_assignedCount_eq_zero line 49
  4. theorem OAI.CycleClique.Construction.ExpandedPathSystem.assignedCount_pos_of_amount_pos line 55
  5. theorem OAI.CycleClique.Construction.ExpandedPathSystem.incident_eq_two_of_assignedCount_one line 62