OAI/Probability/SwitchChain/DisjointReconstruct.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem315.DisjointEncoding.blockEquiv line 12
  2. theorem OAI.Problem315.DisjointEncoding.blockEquiv_inl line 26
  3. theorem OAI.Problem315.DisjointEncoding.blockEquiv_inr line 29
  4. theorem OAI.Problem315.DisjointEncoding.blockEquiv_symm_endpoint line 32
  5. theorem OAI.Problem315.DisjointEncoding.blockEquiv_symm_outside line 36
  6. def OAI.Problem315.DisjointEncoding.glueGraph line 40
  7. def OAI.Problem315.DisjointEncoding.reconstruct line 60
  8. theorem OAI.Problem315.DisjointEncoding.reconstruct_block_block line 65
  9. theorem OAI.Problem315.DisjointEncoding.reconstruct_block_outside line 71
  10. theorem OAI.Problem315.DisjointEncoding.reconstruct_outside_block line 77
  11. theorem OAI.Problem315.DisjointEncoding.reconstruct_outside_outside line 83
  12. theorem OAI.Problem315.DisjointEncoding.reconstruct_graph line 89
  13. def OAI.Problem315.DisjointEncoding.BoundaryMatches line 97
  14. theorem OAI.Problem315.DisjointEncoding.sameCell_reconstruct line 104
  15. theorem OAI.Problem315.DisjointEncoding.degree_eq_sum_bits line 130
  16. theorem OAI.Problem315.DisjointEncoding.degree_reconstruct_block line 134
  17. theorem OAI.Problem315.DisjointEncoding.degree_reconstruct_outside line 146
  18. theorem OAI.Problem315.DisjointEncoding.degree_outside_preserved line 158
  19. theorem OAI.Problem315.DisjointEncoding.degree_preserved_of_block line 176