OAI/Combinatorics/BalancedRyser/Construction/Construction.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.Slot line 15
  2. abbrev OAI.Balanced.MergedPairs line 16
  3. structure OAI.Balanced.FourTuple line 18
  4. structure OAI.Balanced.SplitChoice line 23
  5. structure OAI.Balanced.Configuration line 28
  6. instance OAI.Balanced.(instance at line 33) line 33
  7. instance OAI.Balanced.(instance at line 40) line 40
  8. instance OAI.Balanced.(instance at line 47) line 47
  9. def OAI.Balanced.constituent line 56
  10. def OAI.Balanced.DistinctConstituents line 58
  11. def OAI.Balanced.constituentLines line 61
  12. def OAI.Balanced.mergedPoints line 64
  13. def OAI.Balanced.tuplePoint line 67
  14. def OAI.Balanced.designated line 71
  15. def OAI.Balanced.generatorSet line 74
  16. def OAI.Balanced.Adjacent line 77
  17. def OAI.Balanced.ValidChoice line 82
  18. def OAI.Balanced.Configuration.Valid line 97
  19. def OAI.Balanced.Configuration.Compatible line 100
  20. def OAI.Balanced.Configuration.splitLines line 108
  21. def OAI.Balanced.Configuration.deletedLines line 110
  22. def OAI.Balanced.Configuration.core line 113
  23. def OAI.Balanced.Configuration.retained line 116
  24. def OAI.Balanced.Configuration.points line 119
  25. def OAI.Balanced.Configuration.splitLinesAt line 122
  26. def OAI.Balanced.Configuration.splitMultiplicity line 125
  27. def OAI.Balanced.Configuration.designatedAt line 127
  28. def OAI.Balanced.Configuration.partnerSet line 131
  29. def OAI.Balanced.Configuration.Occupancy line 136
  30. def OAI.Balanced.Configuration.CoreConcentration line 142
  31. abbrev OAI.Balanced.LocalPiece line 150
  32. def OAI.Balanced.Configuration.localPiecePoints line 156
  33. def OAI.Balanced.Configuration.AllowedLocalPiece line 161
  34. def OAI.Balanced.Configuration.LocalCondition line 166
  35. abbrev OAI.Balanced.Configuration.BlockLabel line 172
  36. def OAI.Balanced.Configuration.blockDirection line 174
  37. def OAI.Balanced.Configuration.blockPoints line 179
  38. def OAI.Balanced.Configuration.IsBlockLabel line 187
  39. def OAI.Balanced.Configuration.blockLabels line 191
  40. def OAI.Balanced.Configuration.labelsInDirection line 194