OAI/Geometry/IsometricImmersion/Calculus/CoordinateJetReverseNorm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Geometry.coordinate_basis_decomposition line 12
2. theorem OAI.SmoothLocal.Geometry.multilinear_coordinate_components line 17
3. theorem OAI.SmoothLocal.Geometry.multilinear_norm_le_coordinate_bound line 35
4. theorem OAI.SmoothLocal.Geometry.full_jet_norm_le_coordinate_words line 57
5. theorem OAI.SmoothLocal.Geometry.CoordinateBound.full_jet_norm_bound line 67