OAI/Geometry/IsometricImmersion/Darboux/QSegmentDomain.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.qHeightJetSegment line 14
  2. theorem OAI.SmoothLocal.HighEquation.stateSegment_zero line 17
  3. theorem OAI.SmoothLocal.HighEquation.stateSegment_one line 20
  4. theorem OAI.SmoothLocal.HighEquation.stateSegment_hasDerivAt line 23
  5. theorem OAI.SmoothLocal.HighEquation.stateSegment_continuous line 32
  6. theorem OAI.SmoothLocal.HighEquation.statePoint_qHeightJetSegment line 35
  7. theorem OAI.SmoothLocal.HighEquation.stateQDenominator_segment line 40
  8. theorem OAI.SmoothLocal.HighEquation.stateQDenominator_difference line 51
  9. theorem OAI.SmoothLocal.HighEquation.stateQDenominator_segment_error line 60
  10. theorem OAI.SmoothLocal.HighEquation.stateQDenominator_segment_lower line 72
  11. theorem OAI.SmoothLocal.HighEquation.stateQDenominator_bound line 83
  12. theorem OAI.SmoothLocal.HighEquation.state_distance_le_of_coordinate_error line 97
  13. theorem OAI.SmoothLocal.HighEquation.qSolutionJet_coordinate_error line 104
  14. theorem OAI.SmoothLocal.HighEquation.qHeightJetSegment_denominator_lower line 121