OAI/Geometry/QuadricBundles/Gluing.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.QuadricCounterexample.matrix_coefficients_inverse line 12
2. lemma OAI.QuadricCounterexample.traceScalar_tendsto line 15
3. def OAI.QuadricCounterexample.coefficientFrame line 25
4. lemma OAI.QuadricCounterexample.coefficientFrame_continuousOn line 29
5. lemma OAI.QuadricCounterexample.coefficientFrame_bounded line 38
6. lemma OAI.QuadricCounterexample.ExtractedTrace.coefficients_eq line 48
7. lemma OAI.QuadricCounterexample.ExtractedTrace.coefficients_change line 53
8. lemma OAI.QuadricCounterexample.ExtractedTrace.weak_coefficients_change line 70
9. lemma OAI.QuadricCounterexample.coordinateChange_differentiableOn line 158
10. lemma OAI.QuadricCounterexample.coordinateFiberChange_differentiableOn line 172
11. lemma OAI.QuadricCounterexample.ExtractedTrace.globalValue_representative_ae line 189
12. lemma OAI.QuadricCounterexample.ExtractedTrace.globalValue_composed_representative_ae line 201
13. lemma OAI.QuadricCounterexample.ExtractedTrace.coefficientFrame_quadraticValue line 219
14. lemma OAI.QuadricCounterexample.ExtractedTrace.globalValue_change_ae_indices line 225
15. lemma OAI.QuadricCounterexample.ExtractedTrace.globalValue_change_ae line 247
16. lemma OAI.QuadricCounterexample.ExtractedTrace.globalValue_change line 258