OAI/Geometry/IntegralFillings/Slicing/CoordinateDerivative.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.IntegerChart.coordinateSlice_scalar_eq line 33
2. lemma OAI.SharpIntegralFillings.IntegerChart.coordinateSlice_fderiv line 41
3. lemma OAI.SharpIntegralFillings.IntegerChart.ae_coordinateSlice_fderiv line 76
4. def OAI.SharpIntegralFillings.IntegerChart.coordinateEmptyChart line 110
5. def OAI.SharpIntegralFillings.IntegerChart.coordinateSliceTotal line 125
6. lemma OAI.SharpIntegralFillings.IntegerChart.ae_coordinateSliceTotal_eq line 131