OAI/Geometry/Kahler/HartogsCurvatureContinuity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PinchedHartogs.hermitianValue_pairValue line 21
2. lemma OAI.PinchedHartogs.realArea_positive line 30
3. lemma OAI.PinchedHartogs.metric_isHermitian line 45
4. lemma OAI.PinchedHartogs.curvature_continuousAt line 50
5. lemma OAI.PinchedHartogs.tensorValue_continuousAt line 75
6. lemma OAI.PinchedHartogs.hermitianValue_continuousAt line 90
7. lemma OAI.PinchedHartogs.sectional_continuousAt line 99