OAI/Geometry/SmoothYau/Smoothness/NormalInverseVecNorm.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.YauCounterexamples.smooth_open_inverse line 45
2. lemma OAI.YauCounterexamples.familyTotal_derivative_invertible line 88
3. lemma OAI.YauCounterexamples.isOpen_continuousLinearMap_isInvertible line 116
4. lemma OAI.YauCounterexamples.normalJetMap_injOn_small line 170
5. def OAI.YauCounterexamples.normalFamilySource line 206
6. def OAI.YauCounterexamples.normalFamilyTotal line 210
7. lemma OAI.YauCounterexamples.isOpen_normalFamilySource line 214
8. lemma OAI.YauCounterexamples.normalFamilyTotal_injOn line 238
9. lemma OAI.YauCounterexamples.normalFamilyTotal_smooth line 254
10. lemma OAI.YauCounterexamples.normalFamilyTotal_derivative_invertible line 257
11. theorem OAI.YauCounterexamples.exists_normal_family_inverse line 278
12. lemma OAI.YauCounterexamples.compact_normal_family_radius line 285