OAI/Geometry/IsometricImmersion/Calculus/StateJetSegment.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.HighEquation.stateSegment line 13
  2. def OAI.SmoothLocal.HighEquation.heightJetSegment line 16
  3. theorem OAI.SmoothLocal.HighEquation.statePoint_segment line 19
  4. theorem OAI.SmoothLocal.HighEquation.statePoint_heightJetSegment line 28
  5. theorem OAI.SmoothLocal.HighEquation.stateDenominator_segment line 33
  6. theorem OAI.SmoothLocal.HighEquation.stateMixed_segment line 44
  7. theorem OAI.SmoothLocal.HighEquation.stateDenominator_heightJetSegment line 55
  8. theorem OAI.SmoothLocal.HighEquation.stateDenominator_difference line 63
  9. theorem OAI.SmoothLocal.HighEquation.stateMixed_difference line 72
  10. theorem OAI.SmoothLocal.HighEquation.three_term_jet_error line 81
  11. theorem OAI.SmoothLocal.HighEquation.affine_segment_error line 99
  12. theorem OAI.SmoothLocal.HighEquation.stateDenominator_segment_error line 107
  13. theorem OAI.SmoothLocal.HighEquation.stateMixed_segment_error line 120
  14. theorem OAI.SmoothLocal.HighEquation.denominator_lower_of_error line 133
  15. theorem OAI.SmoothLocal.HighEquation.heightJetSegment_denominator_lower line 141
  16. theorem OAI.SmoothLocal.HighEquation.heightJetSegment_mem_domain line 157
  17. theorem OAI.SmoothLocal.HighEquation.quotient_difference_bound line 166
  18. theorem OAI.SmoothLocal.HighEquation.stateSegment_quotient_error line 185