OAI/Geometry/SmoothYau/Smoothness/ContDiffMetricFluxC1.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.contDiffAt_metricFlux_C1 line 21
2. lemma OAI.YauCounterexamples.contDiff_realChartLocalize_C2 line 34
3. lemma OAI.YauCounterexamples.localGradientPair_change_C2 line 46
4. lemma OAI.YauCounterexamples.coordinateGradientPair_inChart_C2 line 76
5. lemma OAI.YauCounterexamples.contMDiff_coordinateGradientPair_C1 line 95