OAI/Analysis/SymmetricDomains/Basic.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Release061.Affine line 8

    Also declared: ComparatorChallenges/SymmetricDomains.lean:7 (same declaration text).

  2. def OAI.Release061.realCoordinates line 10

    Also declared: ComparatorChallenges/SymmetricDomains.lean:9 (same declaration text).

  3. def OAI.Release061.IsAffineAlgebraic line 13

    Also declared: ComparatorChallenges/SymmetricDomains.lean:12 (same declaration text).

  4. inductive OAI.Release061.IsSemialgebraic line 17

    Also declared: ComparatorChallenges/SymmetricDomains.lean:16 (same declaration text).

  5. def OAI.Release061.HolomorphicOnSubset line 26

    Also declared: ComparatorChallenges/SymmetricDomains.lean:25 (same declaration text).

  6. structure OAI.Release061.Biholomorph line 31

    Also declared: ComparatorChallenges/SymmetricDomains.lean:30 (same declaration text).

  7. def OAI.Release061.IsSmooth line 36

    Also declared: ComparatorChallenges/SymmetricDomains.lean:35 (same declaration text).

  8. def OAI.Release061.IsBoundedSymmetricDomain line 41

    Also declared: ComparatorChallenges/SymmetricDomains.lean:40 (same declaration text).

  9. theorem OAI.Release061.IsAffineAlgebraic.isClosed line 48
  10. theorem OAI.Release061.locallyCompact_of_relative_open line 56
  11. theorem OAI.Release061.exists_compact_orbit_representatives line 75
  12. theorem OAI.Release061.HolomorphicOnSubset.continuous line 100
  13. theorem OAI.Release061.HolomorphicOnSubset.comp line 109
  14. theorem OAI.Release061.holomorphicOnSubset_val line 130
  15. def OAI.Release061.Biholomorph.refl line 138
  16. def OAI.Release061.Biholomorph.symm line 143
  17. def OAI.Release061.Biholomorph.trans line 149
  18. theorem OAI.Release061.analytic_coefficient_difference_bound line 158
  19. theorem OAI.Release061.coalescing_root_bound line 176
  20. theorem OAI.Release061.equicontinuousAt_of_coalescing_polynomials line 201