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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Count the incident clique vertices after isolated chain pieces are removed.

  1. def OAI.CycleClique.Construction.activeCliqueCount line 14
  2. theorem OAI.CycleClique.Construction.activeCliqueCount_nil line 17
  3. theorem OAI.CycleClique.Construction.activeCliqueCount_singleton line 20
  4. theorem OAI.CycleClique.Construction.activeCliqueCount_reverse line 23
  5. theorem OAI.CycleClique.Construction.activeCliqueCount_add_singleton line 27
  6. theorem OAI.CycleClique.Construction.RawPathSystem.normalize_incident line 50
  7. theorem OAI.CycleClique.Construction.RawPathSystem.orientChains_normalize_incident line 62
  8. theorem OAI.CycleClique.Construction.RawPathSystem.reorder_normalize_incident line 74
  9. theorem OAI.CycleClique.Construction.RawPathSystem.completeClique_normalize_incident line 80
  10. theorem OAI.CycleClique.Construction.ExpandedPathSystem.toRaw_normalize_incident line 90