OAI/Geometry/IsometricImmersion/Calculus/MixedCoordinateCalculus.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SmoothLocal.HighEquation.orderedPartial_contDiffOn line 15
  2. theorem OAI.SmoothLocal.HighEquation.orderedPartial_append line 24
  3. theorem OAI.SmoothLocal.HighEquation.orderedPartial_perm line 32
  4. theorem OAI.SmoothLocal.HighEquation.coordinateDirections_apply line 54
  5. theorem OAI.SmoothLocal.HighEquation.fullJet_coordinate_inputs_eq_ordered line 63
  6. theorem OAI.SmoothLocal.HighEquation.state_fullJet_eval line 86
  7. theorem OAI.SmoothLocal.HighEquation.fullJet_linear_zero line 96
  8. theorem OAI.SmoothLocal.HighEquation.solutionJet_fullJet_ge_two line 111
  9. theorem OAI.SmoothLocal.HighEquation.solutionJet_fullJet_one line 131
  10. theorem OAI.SmoothLocal.HighEquation.word_two_x_permutation line 154
  11. theorem OAI.SmoothLocal.HighEquation.mixed_principal_word_orders line 165