OAI/Geometry/Kahler/BaseProjective.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PinchedHartogs.BaseConstruction.projectiveDistance line 20
2. def OAI.PinchedHartogs.BaseConstruction.bloch line 22
3. lemma OAI.PinchedHartogs.BaseConstruction.bloch_continuous line 24
4. lemma OAI.PinchedHartogs.BaseConstruction.bracket_coordinates line 33
5. lemma OAI.PinchedHartogs.BaseConstruction.bracket_radial_identity line 36
6. lemma OAI.PinchedHartogs.BaseConstruction.bloch_dist_sq line 44
7. lemma OAI.PinchedHartogs.BaseConstruction.projectiveDistance_eq_dist line 59
8. lemma OAI.PinchedHartogs.BaseConstruction.projectiveDistance_triangle line 62
9. lemma OAI.PinchedHartogs.BaseConstruction.projectiveDistance_nonneg line 67
10. lemma OAI.PinchedHartogs.BaseConstruction.projectiveDistance_symm line 68
11. lemma OAI.PinchedHartogs.BaseConstruction.projectiveDistance_self line 70
12. lemma OAI.PinchedHartogs.BaseConstruction.projectiveDistance_continuous line 73
13. lemma OAI.PinchedHartogs.BaseConstruction.bracket_norm_le_one line 76
14. lemma OAI.PinchedHartogs.BaseConstruction.projectiveDistance_sq line 79
15. lemma OAI.PinchedHartogs.BaseConstruction.projectiveDistance_le_one line 82
16. def OAI.PinchedHartogs.BaseConstruction.adaptedIsometry line 87
17. lemma OAI.PinchedHartogs.BaseConstruction.adaptedIsometry_zero line 91
18. lemma OAI.PinchedHartogs.BaseConstruction.adapted_radialU line 95
19. lemma OAI.PinchedHartogs.BaseConstruction.projective_cap_measure line 98