OAI/Geometry/KahlerSplitting/HolomorphicIdentity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniversalCoverSplitting.holomorphic_eqOn_of_convex_of_eventuallyEq line 35
2. theorem OAI.UniversalCoverSplitting.holomorphic_eqOn_of_preconnected_of_eventuallyEq line 61
3. theorem OAI.UniversalCoverSplitting.holomorphic_manifold_eqOn_of_preconnected_of_eventuallyEq line 90
4. theorem OAI.UniversalCoverSplitting.holomorphic_manifolds_eqOn_of_preconnected_of_eventuallyEq line 144
5. theorem OAI.UniversalCoverSplitting.independent_second_of_fderiv_zero line 199
6. theorem OAI.UniversalCoverSplitting.finite_curveArea_removable_at line 235
7. theorem OAI.UniversalCoverSplitting.finite_curveArea_remove_finite line 274
8. theorem OAI.UniversalCoverSplitting.bounded_curveArea_subsequence_with_removed_limit line 323