OAI/Analysis/BiholderTransport/Coordinates/ChartTransition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.hasFDerivAt_chart_transition line 65
2. lemma OAI.WeakMTWTransport.contDiffAt_chart_transition line 73
3. lemma OAI.WeakMTWTransport.chart_transition_derivative_surjective line 87
4. lemma OAI.WeakMTWTransport.symmL_chart_transition line 98
5. lemma OAI.WeakMTWTransport.chart_metric_transition line 122
6. lemma OAI.WeakMTWTransport.tangent_chart_apply line 149
7. lemma OAI.WeakMTWTransport.tangent_chart_symm_base line 154
8. lemma OAI.WeakMTWTransport.tangent_chart_symm_fiber line 158
9. lemma OAI.WeakMTWTransport.tangent_chart_transition_apply line 164