OAI/Computability/PerfectCompleteness/Foundations/GeometricPrefixSplit.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.GeometricPrefixSplit.depthEquiv line 17
  2. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.castPath_step line 30
  3. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.depthEquiv_path line 38
  4. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.castPath_trans line 54
  5. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.prefixPathDepth_cast line 61
  6. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.castPath_append line 68
  7. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.castPath_depth_append line 74
  8. def OAI.PerfectCompleteness.GeometricPrefixSplit.splitEquiv line 86
  9. def OAI.PerfectCompleteness.GeometricPrefixSplit.joinEquiv line 94
  10. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.split_join line 98
  11. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.join_split line 103
  12. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.prefixPath_split line 108
  13. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.prefixPath_split_spec line 145
  14. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.prefixPath_join line 153
  15. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.law_split line 162
  16. theorem OAI.PerfectCompleteness.GeometricPrefixSplit.expectation_split line 177