OAI/Probability/SwitchChain/TripleGraphEncoding.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.TripleInternalEncoding.adjacencyBit line 12
  2. def OAI.Problem315.TripleInternalEncoding.leftDegree line 15
  3. def OAI.Problem315.TripleInternalEncoding.crossColumn line 18
  4. def OAI.Problem315.TripleInternalEncoding.internalGraph line 21
  5. def OAI.Problem315.TripleInternalEncoding.outsideGraph line 24
  6. theorem OAI.Problem315.TripleInternalEncoding.leftDegree_eq_degree line 27
  7. theorem OAI.Problem315.TripleInternalEncoding.leftDegree_decompose line 32
  8. abbrev OAI.Problem315.TripleInternalEncoding.GraphTripleCell line 38
  9. def OAI.Problem315.TripleInternalEncoding.graphToCell line 45
  10. def OAI.Problem315.TripleInternalEncoding.assembleGraph line 56
  11. theorem OAI.Problem315.TripleInternalEncoding.internalGraph_assemble line 82
  12. theorem OAI.Problem315.TripleInternalEncoding.outsideGraph_assemble line 87
  13. theorem OAI.Problem315.TripleInternalEncoding.adjacencyBit_assemble_cross line 92
  14. def OAI.Problem315.TripleInternalEncoding.cellToGraph line 102
  15. theorem OAI.Problem315.TripleInternalEncoding.graphToCell_cellToGraph line 114
  16. theorem OAI.Problem315.TripleInternalEncoding.cellToGraph_graphToCell line 121
  17. def OAI.Problem315.TripleInternalEncoding.graphTripleCellEquiv line 139
  18. def OAI.Problem315.TripleInternalEncoding.graphTripleMatrixEquiv line 146