OAI/Combinatorics/IndependentSets/Encoding/Occurrences.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding line 10
  2. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding.fin line 16
  3. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding.bool line 17
  4. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding.unit line 18
  5. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding.prod line 20
  6. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding.sum line 23
  7. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding.function line 26
  8. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding.enumerate line 34
  9. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding.length_enumerate line 36
  10. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding.mem_enumerate line 39
  11. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding.nodup_enumerate line 43
  12. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.Encoding.card_eq_size line 46
  13. abbrev OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.GlobalKey line 52
  14. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.globalEncoding line 54
  15. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.globalEncoding_size line 60
  16. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.extendRestricted line 65
  17. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.extendRestricted_valid line 69
  18. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.extendRestricted_injective line 73
  19. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.restrictQuery_extendRestricted line 80
  20. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.canonicalInput_half line 86
  21. def OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey line 92
  22. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_code line 97
  23. theorem OAI.IndependentSetsGames.Foundations.Hastad.SourceOccurrences.assignmentOfKey_surjective line 103