OAI/Combinatorics/ParityLifts/TableGraphs.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ParityWL.Complexity.ChoiceData line 7
  2. def OAI.ParityWL.Complexity.ChoiceData.entry line 9
  3. def OAI.ParityWL.Complexity.ChoiceData.pairBound line 12
  4. def OAI.ParityWL.Complexity.ChoiceData.label line 15
  5. lemma OAI.ParityWL.Complexity.ChoiceData.pairBound_symm line 18
  6. def OAI.ParityWL.Complexity.ChoiceData.system line 21
  7. def OAI.ParityWL.Complexity.ChoiceData.roleSize line 35
  8. def OAI.ParityWL.Complexity.ChoiceData.vertex line 39
  9. lemma OAI.ParityWL.Complexity.ChoiceData.vertex_type line 44
  10. def OAI.ParityWL.Complexity.ChoiceData.baseIndex line 47
  11. lemma OAI.ParityWL.Complexity.ChoiceData.vertex_index line 51
  12. def OAI.ParityWL.Complexity.ChoiceData.helperTest line 54
  13. def OAI.ParityWL.Complexity.ChoiceData.baseTest line 59
  14. lemma OAI.ParityWL.Complexity.ChoiceData.baseTest_symm line 65
  15. lemma OAI.ParityWL.Complexity.ChoiceData.baseTest_arc line 69
  16. lemma OAI.ParityWL.Complexity.ChoiceData.baseTest_adj line 82
  17. lemma OAI.ParityWL.Complexity.ChoiceData.helperTest_arc line 90
  18. lemma OAI.ParityWL.Complexity.ChoiceData.adj_of_baseTest line 112
  19. lemma OAI.ParityWL.Complexity.ChoiceData.baseTest_iff line 129
  20. def OAI.ParityWL.Complexity.enumPairs line 138
  21. lemma OAI.ParityWL.Complexity.mem_enumPairs line 141
  22. lemma OAI.ParityWL.Complexity.nodup_enumPairs line 145
  23. def OAI.ParityWL.Complexity.enumPairsEquiv line 156
  24. lemma OAI.ParityWL.Complexity.enumPairsEquiv_fst line 163
  25. lemma OAI.ParityWL.Complexity.enumPairsEquiv_snd line 165
  26. abbrev OAI.ParityWL.Complexity.GlobalTag line 168
  27. abbrev OAI.ParityWL.Complexity.TagIndex line 170
  28. def OAI.ParityWL.Complexity.tagDecode line 172
  29. def OAI.ParityWL.Complexity.ChoiceData.globalLiftEquiv line 175
  30. def OAI.ParityWL.Complexity.ChoiceData.indexSize line 187
  31. def OAI.ParityWL.Complexity.ChoiceData.vertices line 190
  32. def OAI.ParityWL.Complexity.ChoiceData.vertexEquiv line 193
  33. def OAI.ParityWL.Complexity.ChoiceData.indexedGraph line 199
  34. def OAI.ParityWL.Complexity.ChoiceData.indexedIso line 203
  35. def OAI.ParityWL.Complexity.tagTest line 207
  36. def OAI.ParityWL.Complexity.ChoiceData.edgeTest line 211
  37. lemma OAI.ParityWL.Complexity.ChoiceData.lift_arc_iff line 216
  38. lemma OAI.ParityWL.Complexity.ChoiceData.globalLift_raw line 237
  39. lemma OAI.ParityWL.Complexity.ChoiceData.vertexEquiv_raw line 244
  40. lemma OAI.ParityWL.Complexity.ChoiceData.indexed_adj line 251