OAI/Computability/PerfectCompleteness/Foundations/OriginalWholeCutBridge.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.OriginalWholeCutBridge.pair_map_transport line 17
  2. theorem OAI.PerfectCompleteness.OriginalWholeCutBridge.product_pair_map line 30
  3. def OAI.PerfectCompleteness.OriginalWholeCutBridge.assembledEquiv line 51
  4. def OAI.PerfectCompleteness.OriginalWholeCutBridge.scalarValuesLaw line 56
  5. theorem OAI.PerfectCompleteness.OriginalWholeCutBridge.observed_product_law line 62
  6. abbrev OAI.PerfectCompleteness.OriginalWholeCutBridge.NumberedRecord line 96
  7. def OAI.PerfectCompleteness.OriginalWholeCutBridge.numberRecord line 102
  8. def OAI.PerfectCompleteness.OriginalWholeCutBridge.reconstruct line 108
  9. theorem OAI.PerfectCompleteness.OriginalWholeCutBridge.reconstruct_numberRecord line 113
  10. theorem OAI.PerfectCompleteness.OriginalWholeCutBridge.numberRecord_law line 119
  11. theorem OAI.PerfectCompleteness.OriginalWholeCutBridge.reconstruct_child_law line 147
  12. theorem OAI.PerfectCompleteness.OriginalWholeCutBridge.reconstruct_blocks_law line 165