OAI/Combinatorics/BalancedRyser/Local/LocalPatternTransport.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Local.exists_classRelabeling line 16
  2. def OAI.Balanced.Local.relabelAssignment line 28
  3. theorem OAI.Balanced.Local.relabelAssignment_target line 36
  4. theorem OAI.Balanced.Local.relabelAssignment_generator line 42
  5. theorem OAI.Balanced.Local.eligible_relabelAssignment line 49
  6. theorem OAI.Balanced.Local.prescribedTuple_relabelAssignment line 64
  7. theorem OAI.Balanced.Local.prescribedPoint_relabelAssignment line 74
  8. theorem OAI.Balanced.Local.aligned_relabelAssignment line 82
  9. theorem OAI.Balanced.Local.admissible_relabelAssignment line 88
  10. theorem OAI.Balanced.Local.prescribedDesignated_relabelAssignment line 95
  11. theorem OAI.Balanced.Local.prescribedPartners_relabelAssignment line 101
  12. theorem OAI.Balanced.Local.allowedPiece_relabelAssignment line 108
  13. theorem OAI.Balanced.Local.badCover_relabelAssignment line 116
  14. theorem OAI.Balanced.Local.admissibleBadCover_relabelAssignment line 122
  15. theorem OAI.Balanced.Local.direction_sum_eq_of_relabeling line 129
  16. theorem OAI.Balanced.Local.conditioned_badCover_eq_of_relabeling line 142
  17. theorem OAI.Balanced.Local.direction_sum_eq_of_same_pattern line 157
  18. def OAI.Balanced.Local.directionBadCoverMass line 173
  19. theorem OAI.Balanced.Local.exists_directionSum_representatives line 180
  20. theorem OAI.Balanced.Local.exists_representative_test_family line 192