OAI/Geometry/KahlerSplitting/Monodromy.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniversalCoverSplitting.FirstGerm.initial line 14
  2. lemma OAI.UniversalCoverSplitting.FirstGerm.initial_base line 20
  3. lemma OAI.UniversalCoverSplitting.FirstGerm.initial_first line 24
  4. lemma OAI.UniversalCoverSplitting.FirstGerm.initial_eq line 28
  5. lemma OAI.UniversalCoverSplitting.FirstGerm.continuous_horizontal line 33
  6. lemma OAI.UniversalCoverSplitting.FirstGerm.lift_diagonal line 56
  7. lemma OAI.UniversalCoverSplitting.FirstGerm.lift_path line 77
  8. def OAI.FunctionEtale.value line 102
  9. lemma OAI.FunctionEtale.value_section line 105
  10. def OAI.UniversalCoverSplitting.HolomorphicEtale.value line 113
  11. lemma OAI.UniversalCoverSplitting.HolomorphicEtale.value_of_section line 115
  12. lemma OAI.UniversalCoverSplitting.HolomorphicEtale.mdifferentiable_value line 119
  13. lemma OAI.UniversalCoverSplitting.HolomorphicEtale.value_locally line 132
  14. lemma OAI.UniversalCoverSplitting.LocalBiholomorphism.mdifferentiable line 142
  15. lemma OAI.IsLocalHomeomorph.lift_of_simplyConnected line 159
  16. lemma OAI.UniversalCoverSplitting.LocalBiholomorphism.mdifferentiable_lift line 199
  17. lemma OAI.UniversalCoverSplitting.OrdinaryUniversalCover.holomorphic_lift line 216