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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A finite layout is verified by its chain lengths, clique-position masks and exhaustive indexing. Its realization then uses the actual chain vertices.

  1. theorem OAI.CycleClique.Construction.chainCollection_eq_of_flatten_lengths line 13
  2. def OAI.CycleClique.Construction.layoutGraph line 30
  3. instance OAI.CycleClique.Construction.(instance at line 41) line 41
  4. theorem OAI.CycleClique.Construction.RawPathSystem.realize_layout line 46