OAI/Probability/ClassicalON/LatticeRestriction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.LatticeGraph.restrictVertices line 10
  2. def OAI.ClassicalON.LatticeGraph.restrictVertex line 12
  3. def OAI.ClassicalON.LatticeGraph.restrict line 15
  4. def OAI.ClassicalON.LatticeGraph.restrictEdge line 21
  5. def OAI.ClassicalON.LatticeGraph.restrictVertexEquiv line 24
  6. def OAI.ClassicalON.LatticeGraph.restrictEdgeEquiv line 31
  7. theorem OAI.ClassicalON.LatticeGraph.restrictVertexEquiv_val line 41
  8. theorem OAI.ClassicalON.LatticeGraph.restrictEdgeEquiv_left line 44
  9. theorem OAI.ClassicalON.LatticeGraph.restrictEdgeEquiv_right line 48
  10. def OAI.ClassicalON.LatticeGraph.translateVertexEquiv line 52
  11. def OAI.ClassicalON.LatticeGraph.translate line 56
  12. def OAI.ClassicalON.LatticeGraph.translateEdgeEquiv line 73
  13. theorem OAI.ClassicalON.LatticeGraph.translateVertexEquiv_val line 76
  14. theorem OAI.ClassicalON.LatticeGraph.translateEdgeEquiv_left line 79
  15. theorem OAI.ClassicalON.LatticeGraph.translateEdgeEquiv_right line 82