OAI/NumberTheory/PiExponent/Geometry/CurveNormalizationProper.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.CurveNormalizationModel.parameterOverlapProjection line 15
2. theorem OAI.PiExponent.CurveNormalizationModel.zeroOverlap_projection line 20
3. theorem OAI.PiExponent.CurveNormalizationModel.infinityOverlap_projection line 36
4. def OAI.PiExponent.CurveNormalizationModel.parameterCurveProjection line 59
5. theorem OAI.PiExponent.CurveNormalizationModel.zeroChart_projection line 67
6. theorem OAI.PiExponent.CurveNormalizationModel.infinityChart_projection line 72
7. theorem OAI.PiExponent.CurveNormalizationModel.parameterCurveProjection_preimage_zero line 78
8. theorem OAI.PiExponent.CurveNormalizationModel.parameterCurveProjection_preimage_infinity line 102
9. theorem OAI.PiExponent.CurveNormalizationModel.zeroChartProjection_isPullback line 126
10. theorem OAI.PiExponent.CurveNormalizationModel.infinityChartProjection_isPullback line 132
11. instance OAI.PiExponent.CurveNormalizationModel.parameterCurveProjection_isFinite line 139
12. def OAI.PiExponent.CurveNormalizationModel.parameterCurveStructureMap line 160
13. instance OAI.PiExponent.CurveNormalizationModel.parameterCurveStructureMap_isProper line 163