OAI/Computability/PerfectCompleteness/Foundations/SourcePrefixComparison.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.SourcePrefixComparison.variation_triangle line 18
  2. theorem OAI.PerfectCompleteness.SourcePrefixComparison.sigma_product_forget line 27
  3. def OAI.PerfectCompleteness.SourcePrefixComparison.hiddenError line 45
  4. def OAI.PerfectCompleteness.SourcePrefixComparison.error line 48
  5. def OAI.PerfectCompleteness.SourcePrefixComparison.nativeAssembledLaw line 55
  6. def OAI.PerfectCompleteness.SourcePrefixComparison.uniformLaw line 63
  7. def OAI.PerfectCompleteness.SourcePrefixComparison.continuedLaw line 70
  8. theorem OAI.PerfectCompleteness.SourcePrefixComparison.false_observation_law line 78
  9. theorem OAI.PerfectCompleteness.SourcePrefixComparison.continued_uniform_variation line 85
  10. theorem OAI.PerfectCompleteness.SourcePrefixComparison.original_variation line 102
  11. theorem OAI.PerfectCompleteness.SourcePrefixComparison.original_observed_variation line 119
  12. theorem OAI.PerfectCompleteness.SourcePrefixComparison.conditional_variation line 135
  13. abbrev OAI.PerfectCompleteness.SourcePrefixComparison.ExteriorRaw line 156
  14. abbrev OAI.PerfectCompleteness.SourcePrefixComparison.ExteriorObservation line 160
  15. def OAI.PerfectCompleteness.SourcePrefixComparison.originalExteriorLaw line 165
  16. def OAI.PerfectCompleteness.SourcePrefixComparison.observeExterior line 174
  17. theorem OAI.PerfectCompleteness.SourcePrefixComparison.originalExteriorLaw_forget line 179
  18. theorem OAI.PerfectCompleteness.SourcePrefixComparison.originalExteriorLaw_observe line 209
  19. def OAI.PerfectCompleteness.SourcePrefixComparison.continuedExteriorLaw line 240
  20. theorem OAI.PerfectCompleteness.SourcePrefixComparison.exterior_observed_variation line 249