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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

One-vertex representative exclusions from the concrete chain surgery.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.no_one_vertex_raw line 16
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.forbidden_different_chain_one line 22
  3. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.forbidden_same_chain_one line 42