OAI/Combinatorics/BalancedRyser/Local/LocalConfigurationPattern.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.ConfigurationPattern.slots line 13
  2. def OAI.Balanced.Local.ConfigurationPattern.slotEquiv line 16
  3. def OAI.Balanced.Local.ConfigurationPattern.slot line 21
  4. theorem OAI.Balanced.Local.ConfigurationPattern.slot_injective line 24
  5. theorem OAI.Balanced.Local.ConfigurationPattern.slot_onLine line 27
  6. theorem OAI.Balanced.Local.ConfigurationPattern.exists_slot line 31
  7. theorem OAI.Balanced.Local.ConfigurationPattern.slot_direction_injective line 37
  8. theorem OAI.Balanced.Local.ConfigurationPattern.slot_line_eq line 47
  9. def OAI.Balanced.Local.ConfigurationPattern.point line 55
  10. theorem OAI.Balanced.Local.ConfigurationPattern.point_injective line 58
  11. theorem OAI.Balanced.Local.ConfigurationPattern.point_ne_center line 71
  12. theorem OAI.Balanced.Local.ConfigurationPattern.point_image line 80
  13. def OAI.Balanced.Local.ConfigurationPattern.generator line 94
  14. theorem OAI.Balanced.Local.ConfigurationPattern.generator_image line 97
  15. theorem OAI.Balanced.Local.ConfigurationPattern.generator_card_le line 114
  16. theorem OAI.Balanced.Local.ConfigurationPattern.generator_card_eq line 120
  17. def OAI.Balanced.Local.ConfigurationPattern.generatorEquiv line 124
  18. theorem OAI.Balanced.Local.ConfigurationPattern.generator_mem line 130
  19. def OAI.Balanced.Local.ConfigurationPattern.classOf line 135
  20. def OAI.Balanced.Local.ConfigurationPattern.assignedGenerator line 139
  21. theorem OAI.Balanced.Local.ConfigurationPattern.assignedGenerator_injective line 142
  22. theorem OAI.Balanced.Local.ConfigurationPattern.assigned_class line 145
  23. theorem OAI.Balanced.Local.ConfigurationPattern.class_surjective line 150
  24. theorem OAI.Balanced.Local.ConfigurationPattern.class_injective line 163
  25. theorem OAI.Balanced.Local.ConfigurationPattern.assigned_mem_generators line 169
  26. theorem OAI.Balanced.Local.ConfigurationPattern.class_pair_overlap line 177
  27. def OAI.Balanced.Local.ConfigurationPattern.pattern line 191
  28. def OAI.Balanced.Local.ConfigurationPattern.assignment line 197
  29. def OAI.Balanced.Local.ConfigurationPattern.bits line 200
  30. theorem OAI.Balanced.Local.ConfigurationPattern.assignment_eligible line 203
  31. theorem OAI.Balanced.Local.ConfigurationPattern.prescribedTuple_eq line 210
  32. theorem OAI.Balanced.Local.ConfigurationPattern.prescribedPoint_eq line 224
  33. theorem OAI.Balanced.Local.ConfigurationPattern.aligned line 231
  34. theorem OAI.Balanced.Local.ConfigurationPattern.admissible line 239
  35. theorem OAI.Balanced.Local.ConfigurationPattern.prescribedDesignated_eq line 254
  36. theorem OAI.Balanced.Local.ConfigurationPattern.prescribedPartners_eq line 264
  37. theorem OAI.Balanced.Local.ConfigurationPattern.target_line_image line 270
  38. theorem OAI.Balanced.Local.ConfigurationPattern.allowedPiece_iff line 287
  39. theorem OAI.Balanced.Local.ConfigurationPattern.badCover_iff line 296
  40. theorem OAI.Balanced.Local.ConfigurationPattern.exists_pattern_of_not_local line 306