OAI/Computability/PerfectCompleteness/Foundations/ProjectedFiberBackground.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ProjectedFiberBackground.nodeScalarEquiv line 19
  2. theorem OAI.PerfectCompleteness.ProjectedFiberBackground.nodeScalarEquiv_apply line 26
  3. theorem OAI.PerfectCompleteness.ProjectedFiberBackground.update_fiber_transport line 34
  4. def OAI.PerfectCompleteness.ProjectedFiberBackground.scalarEquiv line 52
  5. theorem OAI.PerfectCompleteness.ProjectedFiberBackground.scalarEquiv_apply line 57
  6. theorem OAI.PerfectCompleteness.ProjectedFiberBackground.scalar_uniform line 63
  7. theorem OAI.PerfectCompleteness.ProjectedFiberBackground.replace_replace line 77
  8. theorem OAI.PerfectCompleteness.ProjectedFiberBackground.arraysAt_eq_native_replace line 93
  9. theorem OAI.PerfectCompleteness.ProjectedFiberBackground.arraysAt_eq_fiber line 105
  10. theorem OAI.PerfectCompleteness.ProjectedFiberBackground.pullback_arraysAt line 121
  11. theorem OAI.PerfectCompleteness.ProjectedFiberBackground.form_at_fiber line 136