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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Hypothetical outside parameters zero and one become, respectively, a required edge and a fresh common neighbor in a finite labelled state.

  1. def OAI.CycleClique.Construction.addedEdgeGraph line 11
  2. instance OAI.CycleClique.Construction.(instance at line 22) line 22
  3. def OAI.CycleClique.Construction.freshGraph line 25
  4. instance OAI.CycleClique.Construction.(instance at line 41) line 41
  5. def OAI.CycleClique.Construction.freshMatrix line 47
  6. def OAI.CycleClique.Construction.addedEdgeHom line 52
  7. def OAI.CycleClique.Construction.freshHom line 62
  8. theorem OAI.CycleClique.Construction.freshHom_injective line 73
  9. theorem OAI.CycleClique.Construction.freshHom_mem line 88
  10. theorem OAI.CycleClique.Construction.freshMatrix_sound line 97