OAI/Computability/PerfectCompleteness/Foundations/ProjectedFiberRawPair.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ProjectedFiberRawPair.castDirection line 18
  2. def OAI.PerfectCompleteness.ProjectedFiberRawPair.castScalar line 24
  3. theorem OAI.PerfectCompleteness.ProjectedFiberRawPair.castScalar_pivot line 30
  4. theorem OAI.PerfectCompleteness.ProjectedFiberRawPair.update_fiber_transport line 40
  5. def OAI.PerfectCompleteness.ProjectedFiberRawPair.direction line 58
  6. def OAI.PerfectCompleteness.ProjectedFiberRawPair.scalar line 62
  7. def OAI.PerfectCompleteness.ProjectedFiberRawPair.oldScalar line 70
  8. def OAI.PerfectCompleteness.ProjectedFiberRawPair.freshScalar line 76
  9. theorem OAI.PerfectCompleteness.ProjectedFiberRawPair.oldScalar_eq_pivot line 80
  10. theorem OAI.PerfectCompleteness.ProjectedFiberRawPair.first_eq_arraysAt line 97
  11. theorem OAI.PerfectCompleteness.ProjectedFiberRawPair.second_eq_arraysAt line 107
  12. theorem OAI.PerfectCompleteness.ProjectedFiberRawPair.first_pullback line 123
  13. theorem OAI.PerfectCompleteness.ProjectedFiberRawPair.second_pullback line 133
  14. theorem OAI.PerfectCompleteness.ProjectedFiberRawPair.form_upperAt line 148
  15. theorem OAI.PerfectCompleteness.ProjectedFiberRawPair.first_form line 161
  16. theorem OAI.PerfectCompleteness.ProjectedFiberRawPair.second_form line 175