OAI/Geometry/KahlerSplitting/EtaleGerms.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FunctionEtale.Total line 12
  2. def OAI.FunctionEtale.base line 15
  3. def OAI.FunctionEtale.sectionOf line 16
  4. def OAI.FunctionEtale.basic line 18
  5. instance OAI.FunctionEtale.(instance at line 21) line 21
  6. lemma OAI.FunctionEtale.section_eq line 24
  7. lemma OAI.FunctionEtale.isOpen_basic line 29
  8. lemma OAI.FunctionEtale.continuous_section line 32
  9. lemma OAI.FunctionEtale.exists_representative line 40
  10. lemma OAI.FunctionEtale.continuous_base line 44
  11. def OAI.FunctionEtale.chart line 56
  12. lemma OAI.FunctionEtale.isLocalHomeomorph_base line 70
  13. lemma OAI.FunctionEtale.isOpen_of_local line 75
  14. lemma OAI.FunctionEtale.isLocalHomeomorph_restrict line 88
  15. lemma OAI.FunctionEtale.continuous_of_local line 92
  16. lemma OAI.FunctionEtale.locally_represented line 100
  17. def OAI.UniversalCoverSplitting.HolomorphicEtale.IsHolomorphic line 120
  18. abbrev OAI.UniversalCoverSplitting.HolomorphicEtale.Germs line 126
  19. def OAI.UniversalCoverSplitting.HolomorphicEtale.base line 127
  20. lemma OAI.UniversalCoverSplitting.HolomorphicEtale.isOpen_holomorphic line 129
  21. lemma OAI.UniversalCoverSplitting.HolomorphicEtale.localHomeomorph line 139
  22. lemma OAI.UniversalCoverSplitting.HolomorphicEtale.separated line 142
  23. def OAI.UniversalCoverSplitting.HolomorphicEtale.sectionOf line 169
  24. lemma OAI.UniversalCoverSplitting.HolomorphicEtale.continuous_section line 173
  25. lemma OAI.UniversalCoverSplitting.HolomorphicEtale.locally_represented line 178
  26. lemma OAI.UniversalCoverSplitting.SplittingChart.transition_first line 202
  27. def OAI.UniversalCoverSplitting.FirstGerm.IsFirst line 238
  28. lemma OAI.UniversalCoverSplitting.FirstGerm.of_factor line 243
  29. lemma OAI.UniversalCoverSplitting.FirstGerm.congr line 251