OAI/Geometry/Borsuk/MatrixGeometry/FibreHomotopy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BorsukNine.negativeCoordinates line 17
  2. lemma OAI.BorsukNine.Admissible.negativeCoordinates_sum line 21
  3. def OAI.BorsukNine.transportedFibre line 35
  4. def OAI.BorsukNine.centeredFibre line 38
  5. lemma OAI.BorsukNine.centeredFibre_mem line 42
  6. lemma OAI.BorsukNine.transportedFibre_mem line 50
  7. def OAI.BorsukNine.fibreHomotopy line 61
  8. lemma OAI.BorsukNine.fibreHomotopy_zero line 67
  9. lemma OAI.BorsukNine.fibreHomotopy_one line 74
  10. lemma OAI.BorsukNine.Admissible.fibreHomotopy_sum line 82
  11. lemma OAI.BorsukNine.Admissible.fibreHomotopy_boundary_misses line 99