OAI/Geometry/Borsuk/Main.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BorsukNine.Vector9 line 10
  2. def OAI.BorsukNine.coordinates9 line 12
  3. theorem OAI.BorsukNine.coordinates9_sub line 19
  4. theorem OAI.BorsukNine.coordinates9_norm_sq line 24
  5. theorem OAI.BorsukNine.coordinates9_dist line 40
  6. theorem OAI.BorsukNine.coordinates9_isometry line 55
  7. theorem OAI.BorsukNine.continuous_coordinates9 line 59
  8. theorem OAI.BorsukNine.coordinates9_diam line 65
  9. theorem OAI.BorsukNine.coordinates9_cover_pullback line 91
  10. theorem OAI.BorsukNine.euclidean_nine_counterexample line 117