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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The selected internal vertices form a separated packing. In a spanning terminal system they already contradict the independence bound.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.original_chain_in_completion line 18
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.selectedChains_outside line 22
  3. theorem OAI.CycleClique.Construction.ExpandedPathSystem.selectedChains_orientation line 30
  4. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.selectedChains_forbidden line 40
  5. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_spanning_interior_contradiction line 99