OAI/Analysis/SymmetricDomains/HolomorphicLocallyUniformLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Release061.ambientExtend line 33
2. lemma OAI.Release061.ambientExtend_apply line 38
3. lemma OAI.Release061.continuousOn_ambientExtend line 43
4. theorem OAI.Release061.HolomorphicOnSubset.analyticOnNhd_extend line 49
5. theorem OAI.Release061.holomorphicOnSubset_of_local line 59
6. theorem OAI.Release061.holomorphic_chart_limit line 78
7. theorem OAI.Release061.IsSmooth.holomorphic_locally_uniform_limit line 114