OAI/Combinatorics/BalancedRyser/Local/LocalDirectionAssignments.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.Local.DirectionToken line 8
  2. def OAI.Balanced.Local.assignmentFunction line 10
  3. def OAI.Balanced.Local.AllTokensDistinct line 13
  4. def OAI.Balanced.Local.tokenInjectionEquiv line 16
  5. theorem OAI.Balanced.Local.allTokensDistinct_eligible line 27
  6. theorem OAI.Balanced.Local.eligible_not_allTokensDistinct_iff line 41
  7. theorem OAI.Balanced.Local.card_directionToken_two line 62
  8. def OAI.Balanced.Local.crossEqualityEquiv line 72
  9. theorem OAI.Balanced.Local.card_crossEquality line 91
  10. theorem OAI.Balanced.Local.card_any_crossEquality_le line 101
  11. theorem OAI.Balanced.Local.card_eligible_not_allDistinct_two_le line 128
  12. theorem OAI.Balanced.Local.card_token_injections_two_le line 149