OAI/Combinatorics/BalancedRyser/Local/ReusePatternCounting.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.ReusePatternCounting.changedSet line 14
  2. def OAI.Balanced.ReusePatternCounting.fillOn line 17
  3. theorem OAI.Balanced.ReusePatternCounting.changedSet_fillOn_subset line 21
  4. theorem OAI.Balanced.ReusePatternCounting.card_sparse_maps_le line 27
  5. theorem OAI.Balanced.ReusePatternCounting.card_sparse_endomaps_le line 58
  6. def OAI.Balanced.ReusePatternCounting.firstRepresentative line 72
  7. theorem OAI.Balanced.ReusePatternCounting.value_firstRepresentative line 76
  8. theorem OAI.Balanced.ReusePatternCounting.firstRepresentative_le line 81
  9. theorem OAI.Balanced.ReusePatternCounting.firstRepresentative_eq_of_value_eq line 86
  10. theorem OAI.Balanced.ReusePatternCounting.firstRepresentative_eq_iff line 91
  11. theorem OAI.Balanced.ReusePatternCounting.firstRepresentative_idempotent line 99
  12. theorem OAI.Balanced.ReusePatternCounting.representative_image_eq_fixed line 103
  13. theorem OAI.Balanced.ReusePatternCounting.card_representative_image line 114
  14. theorem OAI.Balanced.ReusePatternCounting.card_changed_firstRepresentative line 133
  15. theorem OAI.Balanced.ReusePatternCounting.firstRepresentative_eq_of_same_equalities line 146
  16. abbrev OAI.Balanced.ReusePatternCounting.CanonicalPattern line 158
  17. theorem OAI.Balanced.ReusePatternCounting.exists_canonical_pattern line 161
  18. theorem OAI.Balanced.ReusePatternCounting.card_canonical_patterns_le line 169
  19. theorem OAI.Balanced.ReusePatternCounting.card_four_point_patterns_le line 181