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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A positive amount profile determines exactly which positions in each chain belong to the clique. This is the interface to finite indexed models.

  1. def OAI.CycleClique.Construction.profileMask line 11
  2. def OAI.CycleClique.Construction.cliqueMask line 15
  3. theorem OAI.CycleClique.Construction.cliqueMask_eq_map line 19
  4. theorem OAI.CycleClique.Construction.AssignedAmounts.mask line 26
  5. theorem OAI.CycleClique.Construction.profileMask_length line 41
  6. theorem OAI.CycleClique.Construction.AssignedAmounts.nonempty_length_eq line 48
  7. theorem OAI.CycleClique.Construction.profiles_masks line 53
  8. theorem OAI.CycleClique.Construction.profiles_lengths line 62