OAI/Computability/PerfectCompleteness/Foundations/CutNativeForms.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.CutNativeForms.nodeSlots_fill line 17
  2. theorem OAI.PerfectCompleteness.CutNativeForms.nodeSlots_fill_of_agree line 24
  3. def OAI.PerfectCompleteness.CutNativeForms.spaceCast line 39
  4. def OAI.PerfectCompleteness.CutNativeForms.squareCast line 43
  5. def OAI.PerfectCompleteness.CutNativeForms.dualCast line 47
  6. def OAI.PerfectCompleteness.CutNativeForms.formCast line 52
  7. theorem OAI.PerfectCompleteness.CutNativeForms.dualCast_apply line 56
  8. theorem OAI.PerfectCompleteness.CutNativeForms.formCast_apply line 62
  9. theorem OAI.PerfectCompleteness.CutNativeForms.squareCast_product line 67
  10. theorem OAI.PerfectCompleteness.CutNativeForms.formCast_multiplication line 73
  11. theorem OAI.PerfectCompleteness.CutNativeForms.formRank_formCast line 80
  12. theorem OAI.PerfectCompleteness.CutNativeForms.squareCast_one line 86
  13. theorem OAI.PerfectCompleteness.CutNativeForms.dualCast_one line 93
  14. def OAI.PerfectCompleteness.CutNativeForms.oneElement line 100
  15. theorem OAI.PerfectCompleteness.CutNativeForms.dualCast_normalized line 104
  16. def OAI.PerfectCompleteness.CutNativeForms.projectionCast line 111
  17. theorem OAI.PerfectCompleteness.CutNativeForms.spaceCast_HPullback line 118
  18. theorem OAI.PerfectCompleteness.CutNativeForms.formCast_projection_agreement line 126
  19. theorem OAI.PerfectCompleteness.CutNativeForms.dualCast_projection_agreement line 137
  20. def OAI.PerfectCompleteness.CutNativeForms.nativeDual line 159
  21. def OAI.PerfectCompleteness.CutNativeForms.nativeForm line 164
  22. theorem OAI.PerfectCompleteness.CutNativeForms.nativeForm_multiplication line 169
  23. theorem OAI.PerfectCompleteness.CutNativeForms.nativeForm_rank line 177
  24. theorem OAI.PerfectCompleteness.CutNativeForms.nativeDual_normalized line 183
  25. def OAI.PerfectCompleteness.CutNativeForms.nativeProjection line 193
  26. theorem OAI.PerfectCompleteness.CutNativeForms.nativeForm_projection_agreement line 201
  27. theorem OAI.PerfectCompleteness.CutNativeForms.nativeDual_projection_agreement line 215