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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Counting the selected internal vertices, with one unit of loss for components that contain more than a single amount-two path.

  1. def OAI.CycleClique.Construction.selectedChains line 14
  2. def OAI.CycleClique.Construction.selectionLoss line 17
  3. theorem OAI.CycleClique.Construction.selectedChains_sublist line 20
  4. theorem OAI.CycleClique.Construction.SystemAssignedAmounts.selected_length_bounds line 28
  5. theorem OAI.CycleClique.Construction.ExpandedPathSystem.selectedChains_nodup line 56
  6. theorem OAI.CycleClique.Construction.ExpandedPathSystem.selectedChains_mem_vertices line 60
  7. theorem OAI.CycleClique.Construction.ExpandedPathSystem.selectedChains_large line 64