OAI/Analysis/SphereIsometry/UnitRepresentatives.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Unit representatives, including the zero vector

The fallback unit vector is used only at zero. The exact error identity permits normalization of arbitrary representatives of a unit ultranorm class.

  1. def OAI.Tingley.unitize line 18
  2. theorem OAI.Tingley.unitize_zero line 22
  3. theorem OAI.Tingley.unitize_of_ne_zero line 25
  4. theorem OAI.Tingley.norm_smul_unitize line 29
  5. theorem OAI.Tingley.sub_unitize line 36
  6. theorem OAI.Tingley.norm_sub_unitize line 40