OAI/Geometry/Kahler/HartogsCompletenessSupport.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CompactODE.CurveOn line 25
2. lemma OAI.CompactODE.CurveOn.mono line 29
3. lemma OAI.CompactODE.local_uniform line 33
4. lemma OAI.CompactODE.local_unique line 89
5. lemma OAI.CompactODE.unique_Ioo line 100
6. lemma OAI.CompactODE.compact_uniform line 128
7. lemma OAI.CompactODE.eqOn_piecewise line 152
8. lemma OAI.CompactODE.curveOn_piecewise line 168
9. lemma OAI.CompactODE.curveOn_shift line 189
10. lemma OAI.CompactODE.global_from_intervals line 197
11. theorem OAI.CompactODE.global_of_compact_containment line 220
12. lemma OAI.CompactODE.contDiff_of_hasDerivAt line 299
13. theorem OAI.PinchedHartogs.hartogsMetric_geodesicallyComplete line 319