OAI/Geometry/Kahler/BaseHopf.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PinchedHartogs.BaseConstruction.(instance at line 22) line 22
2. instance OAI.PinchedHartogs.BaseConstruction.(instance at line 23) line 23
3. def OAI.PinchedHartogs.BaseConstruction.circleMeasure line 25
4. instance OAI.PinchedHartogs.BaseConstruction.(instance at line 28) line 28
5. instance OAI.PinchedHartogs.BaseConstruction.(instance at line 30) line 30
6. def OAI.PinchedHartogs.BaseConstruction.torusMeasure line 32
7. instance OAI.PinchedHartogs.BaseConstruction.(instance at line 33) line 33
8. instance OAI.PinchedHartogs.BaseConstruction.(instance at line 34) line 34
9. instance OAI.PinchedHartogs.BaseConstruction.(instance at line 35) line 35
10. def OAI.PinchedHartogs.BaseConstruction.torusAction line 37
11. lemma OAI.PinchedHartogs.BaseConstruction.torusAction_zero line 40
12. lemma OAI.PinchedHartogs.BaseConstruction.torusAction_one line 42
13. lemma OAI.PinchedHartogs.BaseConstruction.torusAction_continuous line 45
14. lemma OAI.PinchedHartogs.BaseConstruction.torusAction_mul line 58
15. def OAI.PinchedHartogs.BaseConstruction.radialSphere line 64
16. lemma OAI.PinchedHartogs.BaseConstruction.radialSphere_zero line 73
17. lemma OAI.PinchedHartogs.BaseConstruction.radialSphere_one line 74
18. lemma OAI.PinchedHartogs.BaseConstruction.radialSphere_continuous line 76
19. def OAI.PinchedHartogs.BaseConstruction.hopf line 85
20. lemma OAI.PinchedHartogs.BaseConstruction.hopf_continuous line 86
21. lemma OAI.PinchedHartogs.BaseConstruction.exists_circle_norm_factor line 91
22. lemma OAI.PinchedHartogs.BaseConstruction.exists_hopf line 100
23. lemma OAI.PinchedHartogs.BaseConstruction.compact_continuous_integrable line 115
24. lemma OAI.PinchedHartogs.BaseConstruction.continuous_compact_integral line 120
25. lemma OAI.PinchedHartogs.BaseConstruction.hopf_integral line 131