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

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Select both internal vertices of a single amount-two component, and otherwise all forward internal representatives of that component.

  1. theorem OAI.CycleClique.Construction.AssignedAmounts.chain_length line 16
  2. theorem OAI.CycleClique.Construction.AssignedAmounts.amount_two_shape line 26
  3. def OAI.CycleClique.Construction.interiorRepresentatives line 41
  4. def OAI.CycleClique.Construction.selectedChain line 44
  5. theorem OAI.CycleClique.Construction.interiorRepresentatives_sublist line 47
  6. theorem OAI.CycleClique.Construction.interiorRepresentatives_outside line 51
  7. theorem OAI.CycleClique.Construction.interiorRepresentatives_length line 58
  8. theorem OAI.CycleClique.Construction.selectedChain_sublist line 63
  9. theorem OAI.CycleClique.Construction.twice_length_le_sum line 69
  10. theorem OAI.CycleClique.Construction.amount_profile_eq_two_of_length_four line 79
  11. theorem OAI.CycleClique.Construction.selectedChain_outside line 95
  12. theorem OAI.CycleClique.Construction.selectedChain_length_bounds line 106