OAI/Combinatorics/ParityLifts/UniformRoles.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ParityWL.Complexity.RawRole line 7
  2. def OAI.ParityWL.Complexity.RoleValid line 9
  3. instance OAI.ParityWL.Complexity.(instance at line 14) line 14
  4. def OAI.ParityWL.Complexity.rawRole line 16
  5. lemma OAI.ParityWL.Complexity.rawRole_valid line 20
  6. def OAI.ParityWL.Complexity.roleDecode line 27
  7. lemma OAI.ParityWL.Complexity.roleDecode_rawRole line 37
  8. lemma OAI.ParityWL.Complexity.rawRole_roleDecode line 43
  9. def OAI.ParityWL.Complexity.roleEquiv line 54
  10. lemma OAI.ParityWL.Complexity.rawRole_injective line 60
  11. def OAI.ParityWL.Complexity.allRoles line 65
  12. lemma OAI.ParityWL.Complexity.mem_allRoles line 68
  13. lemma OAI.ParityWL.Complexity.allRoles_nodup line 78
  14. def OAI.ParityWL.Complexity.rawAdjacent line 82
  15. lemma OAI.ParityWL.Complexity.rawAdjacent_iff line 89
  16. def OAI.ParityWL.Complexity.rawNeighbors line 114
  17. lemma OAI.ParityWL.Complexity.mem_rawNeighbors line 117
  18. lemma OAI.ParityWL.Complexity.rawNeighbors_nodup line 121