OAI/Probability/SwitchChain/DisjointRealization.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.DisjointEncoding.crossCode line 13
  2. def OAI.Problem315.DisjointEncoding.leftAssignment line 16
  3. def OAI.Problem315.DisjointEncoding.rightAssignment line 20
  4. def OAI.Problem315.DisjointEncoding.realizeCoordinates line 24
  5. theorem OAI.Problem315.DisjointEncoding.realizeCoordinates_sameCell line 29
  6. theorem OAI.Problem315.DisjointEncoding.crossCode_realizeCoordinates line 39
  7. theorem OAI.Problem315.DisjointEncoding.leftAssignment_realizeCoordinates line 46
  8. theorem OAI.Problem315.DisjointEncoding.rightAssignment_realizeCoordinates line 61
  9. theorem OAI.Problem315.DisjointEncoding.feasible_coordinates_realized line 76
  10. theorem OAI.Problem315.DisjointEncoding.first_edge_iff_of_counts line 91
  11. theorem OAI.Problem315.DisjointEncoding.graph_eq_of_cell_assignments line 105
  12. theorem OAI.Problem315.DisjointEncoding.realizeCoordinates_encode line 145
  13. structure OAI.Problem315.DisjointEncoding.FeasibleCoordinates line 159
  14. abbrev OAI.Problem315.DisjointEncoding.DegreeCell line 169
  15. def OAI.Problem315.DisjointEncoding.cellEncode line 172
  16. def OAI.Problem315.DisjointEncoding.cellDecode line 187
  17. def OAI.Problem315.DisjointEncoding.degreeCellEquiv line 194