OAI/Probability/SwitchChain/DisjointEncoding.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.DisjointEncoding.edgeBit line 12
  2. theorem OAI.Problem315.DisjointEncoding.edgeBit_eq_iff line 14
  3. def OAI.Problem315.DisjointEncoding.Outside line 18
  4. structure OAI.Problem315.DisjointEncoding.SameCell line 20
  5. structure OAI.Problem315.DisjointEncoding.SameCoordinates line 31
  6. theorem OAI.Problem315.DisjointEncoding.block_to_outside line 39
  7. theorem OAI.Problem315.DisjointEncoding.block_to_block line 57
  8. theorem OAI.Problem315.DisjointEncoding.graph_eq_of_cell_coordinates line 84
  9. theorem OAI.Problem315.DisjointEncoding.SameCell.refl line 99
  10. theorem OAI.Problem315.DisjointEncoding.SameCell.symm line 102
  11. theorem OAI.Problem315.DisjointEncoding.SameCell.trans line 108
  12. def OAI.Problem315.DisjointEncoding.leftIndex line 115
  13. def OAI.Problem315.DisjointEncoding.rightIndex line 117
  14. def OAI.Problem315.DisjointEncoding.encode line 119
  15. theorem OAI.Problem315.DisjointEncoding.sameCoordinates_of_encode_eq line 124
  16. theorem OAI.Problem315.DisjointEncoding.encode_eq_iff line 142
  17. theorem OAI.Problem315.DisjointEncoding.encode_cell_injective line 150