OAI/Geometry/CylinderCovering/Nilpotent/Field.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CylinderCovering.Nilpotent.hasFDerivAt_pair line 12
  2. theorem OAI.CylinderCovering.Nilpotent.signedField_hasFDerivAt line 24
  3. theorem OAI.CylinderCovering.Nilpotent.angularDerivative_square_zero line 43
  4. theorem OAI.CylinderCovering.Nilpotent.signedField_fderiv_square_zero line 49
  5. theorem OAI.CylinderCovering.Nilpotent.signedField_contDiffAt line 54
  6. theorem OAI.CylinderCovering.Nilpotent.signedField_contDiffOn line 76
  7. theorem OAI.CylinderCovering.Nilpotent.signedField_smoothNear line 81
  8. theorem OAI.CylinderCovering.Nilpotent.signedField_on_ray line 86
  9. theorem OAI.CylinderCovering.Nilpotent.angularDerivative_on_ray line 90
  10. theorem OAI.CylinderCovering.Nilpotent.continuous_extension_ray_value line 95
  11. theorem OAI.CylinderCovering.Nilpotent.no_continuous_extension line 119
  12. theorem OAI.CylinderCovering.Nilpotent.signedField_not_continuousAt_apex line 131