OAI/Geometry/CylinderCovering/Barycentric/ProjectionFactor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RadialCoordinates.intercept_gram line 11
  2. theorem OAI.RadialCoordinates.intercept_gram_determinant line 18
  3. theorem OAI.RadialCoordinates.firstDirection_sum line 25
  4. theorem OAI.RadialCoordinates.firstSweep_line_direction line 29
  5. theorem OAI.RadialCoordinates.firstDirection_norm_squared line 35
  6. theorem OAI.RadialCoordinates.firstDirection_ne_zero line 41
  7. theorem OAI.RadialCoordinates.interceptNormal_norm line 48
  8. theorem OAI.RadialCoordinates.interceptNormal_tangent_orthogonal line 54
  9. theorem OAI.RadialCoordinates.firstDirection_normal_inner line 61
  10. theorem OAI.RadialCoordinates.firstDirection_projection_cosine line 67