OAI/Geometry/SmoothYau/Smoothness/ChartTransition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.chartTransition line 38
2. def OAI.YauCounterexamples.coordinateTransitionMatrix line 40
3. def OAI.YauCounterexamples.inverseChartDerivative line 45
4. lemma OAI.YauCounterexamples.invChart_derivative_change line 49
5. lemma OAI.YauCounterexamples.coordinateVector_change line 63
6. lemma OAI.YauCounterexamples.bilinear_sum_matrix line 79
7. lemma OAI.YauCounterexamples.metricCoefficients_change line 90