OAI/Computability/PerfectCompleteness/Decoding/LowerCutScalarProjectionLemmas.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.LowerCutScalarProjection.scalarEquiv_HPullback line 21
  2. theorem OAI.PerfectCompleteness.LowerCutScalarProjection.projectionCast_apply line 35
  3. theorem OAI.PerfectCompleteness.LowerCutScalarProjection.projectionCast_fill line 47
  4. theorem OAI.PerfectCompleteness.LowerCutScalarProjection.inverse_spaceCast_HPullback line 60
  5. theorem OAI.PerfectCompleteness.LowerCutScalarProjection.fill_spaceCast_HPullback line 71
  6. theorem OAI.PerfectCompleteness.LowerCutScalarProjection.scalarEquiv_fill_HPullback line 90
  7. def OAI.PerfectCompleteness.LowerCutScalarProjection.nodeEquiv line 105
  8. theorem OAI.PerfectCompleteness.LowerCutScalarProjection.nodeEquiv_HPullback line 110
  9. theorem OAI.PerfectCompleteness.LowerCutScalarProjection.spaceEquiv_HPullback line 119
  10. theorem OAI.PerfectCompleteness.LowerCutScalarProjection.spaceEquiv_fill_HPullback line 139
  11. def OAI.PerfectCompleteness.SourceQuestionLowerForms.rawCast line 181
  12. theorem OAI.PerfectCompleteness.SourceQuestionLowerForms.rawCast_law line 186
  13. theorem OAI.PerfectCompleteness.SourceQuestionLowerForms.formCast_injective line 192
  14. theorem OAI.PerfectCompleteness.SourceQuestionLowerForms.fullCollision_formCast line 197
  15. abbrev OAI.PerfectCompleteness.SourceQuestionLowerForms.Questions line 213
  16. abbrev OAI.PerfectCompleteness.SourceQuestionLowerForms.Calls line 215
  17. def OAI.PerfectCompleteness.SourceQuestionLowerForms.slots line 217
  18. abbrev OAI.PerfectCompleteness.SourceQuestionLowerForms.Raw line 221
  19. abbrev OAI.PerfectCompleteness.SourceQuestionLowerForms.Form line 225
  20. theorem OAI.PerfectCompleteness.SourceQuestionLowerForms.cutSlots_eq line 228
  21. def OAI.PerfectCompleteness.SourceQuestionLowerForms.rawAtCut line 233
  22. theorem OAI.PerfectCompleteness.SourceQuestionLowerForms.rawAtCut_law line 238
  23. abbrev OAI.PerfectCompleteness.SourceQuestionLowerForms.UpperTable line 255
  24. def OAI.PerfectCompleteness.SourceQuestionLowerForms.first line 264
  25. def OAI.PerfectCompleteness.SourceQuestionLowerForms.second line 273
  26. theorem OAI.PerfectCompleteness.SourceQuestionLowerForms.fullCollision_probability line 283