OAI/Geometry/IsometricImmersion/Calculus/HorizontalJetCalculus.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SmoothLocal.HighEquation.horizontalJetline 13 - theorem
OAI.SmoothLocal.HighEquation.horizontalJet_eq_spatialJetline 18 - theorem
OAI.SmoothLocal.HighEquation.horizontalJet_contDiffOnline 24 - theorem
OAI.SmoothLocal.HighEquation.horizontalPoint_contDiffline 33 - theorem
OAI.SmoothLocal.HighEquation.horizontalJet_slice_hasDerivAtline 38 - theorem
OAI.SmoothLocal.HighEquation.horizontalJet_sliceline 49 - theorem
OAI.SmoothLocal.HighEquation.horizontalJet_coordPartialline 68 - theorem
OAI.SmoothLocal.HighEquation.horizontalJet_two_coordPartialsline 89