OAI/Geometry/CylinderCovering/Nilpotent/Profile.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.Nilpotent.Profile.derivative_apply line 10
  2. theorem OAI.CylinderCovering.Nilpotent.Profile.field_on_ray line 14
  3. theorem OAI.CylinderCovering.Nilpotent.Profile.angle_hasFDerivAt line 18
  4. theorem OAI.CylinderCovering.Nilpotent.Profile.field_hasFDerivAt line 33
  5. theorem OAI.CylinderCovering.Nilpotent.Profile.derivative_square_zero line 51
  6. theorem OAI.CylinderCovering.Nilpotent.Profile.field_fderiv_square_zero line 56
  7. theorem OAI.CylinderCovering.Nilpotent.Profile.tangentAt_iff line 64
  8. theorem OAI.CylinderCovering.Nilpotent.Profile.quadratic_hasDerivAt line 77
  9. theorem OAI.CylinderCovering.Nilpotent.Profile.linear_hasDerivAt line 83
  10. theorem OAI.CylinderCovering.Nilpotent.Profile.quadratic_boundary_tangent line 87
  11. theorem OAI.CylinderCovering.Nilpotent.Profile.quadratic_unique line 92
  12. theorem OAI.CylinderCovering.Nilpotent.Profile.source_profiles line 105