OAI/Geometry/Borsuk/SphereGeometry/HomogeneousLift.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BorsukNine.homogeneousLift line 13
  2. lemma OAI.BorsukNine.homogeneousLift_zero line 16
  3. lemma OAI.BorsukNine.homogeneousLift_unit line 20
  4. lemma OAI.BorsukNine.Admissible.lift_nonneg line 27
  5. lemma OAI.BorsukNine.Admissible.lift_sum line 33
  6. lemma OAI.BorsukNine.Admissible.lift_abs_sum line 44
  7. lemma OAI.BorsukNine.Admissible.lift_le line 48
  8. lemma OAI.BorsukNine.Admissible.lift_norm_le line 54
  9. lemma OAI.BorsukNine.Admissible.lift_even line 60
  10. lemma OAI.BorsukNine.homogeneousLift_smul_pos line 66
  11. lemma OAI.BorsukNine.homogeneousLift_smul_nonneg line 78
  12. lemma OAI.BorsukNine.Admissible.lift_continuous line 84
  13. lemma OAI.BorsukNine.Admissible.lift_orthogonal line 100