OAI/Combinatorics/BalancedRyser/Local/LocalPatternCodes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.PatternCodes.occurrenceEquiv line 14
  2. def OAI.Balanced.Local.PatternCodes.flatClasses line 17
  3. theorem OAI.Balanced.Local.PatternCodes.flatClasses_surjective line 20
  4. def OAI.Balanced.Local.PatternCodes.canonicalCode line 27
  5. theorem OAI.Balanced.Local.PatternCodes.canonicalCode_equalities line 37
  6. theorem OAI.Balanced.Local.PatternCodes.canonicalCode_eq_iff line 46
  7. theorem OAI.Balanced.Local.PatternCodes.classOf_injective line 59
  8. theorem OAI.Balanced.Local.PatternCodes.card_actual_pattern_codes_le line 70
  9. theorem OAI.Balanced.Local.PatternCodes.exists_pattern_representatives line 77
  10. def OAI.Balanced.Local.PatternCodes.relabel line 101
  11. theorem OAI.Balanced.Local.PatternCodes.relabel_classOf line 109
  12. def OAI.Balanced.Local.PatternCodes.classEquiv line 117
  13. theorem OAI.Balanced.Local.PatternCodes.classEquiv_apply line 133