OAI/Geometry/Borsuk/SphereGeometry/TraceSphere.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BorsukNine.matrix_trace_continuous line 13
  2. lemma OAI.BorsukNine.matrix_trace_nonneg line 17
  3. lemma OAI.BorsukNine.positive_ball_image line 20
  4. lemma OAI.BorsukNine.positive_ball_compact line 39
  5. def OAI.BorsukNine.traceSphere line 43
  6. lemma OAI.BorsukNine.traceSphere_closed line 46
  7. lemma OAI.BorsukNine.traceSphere_compact line 50
  8. lemma OAI.BorsukNine.traceSphere_ne_zero line 64
  9. lemma OAI.BorsukNine.traceAbs_pos line 68
  10. def OAI.BorsukNine.traceRadial line 77
  11. lemma OAI.BorsukNine.traceRadial_mem line 79
  12. lemma OAI.BorsukNine.traceRadial_continuousOn line 87
  13. lemma OAI.BorsukNine.traceRadial_neg line 91