OAI/Analysis/SymmetricDomains/SemialgebraicBoundaryFiniteNash.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.realCoordinatesEquiv line 36
  2. def OAI.Release061.complexRealEquiv line 45
  3. lemma OAI.Release061.complexRealEquiv_apply line 49
  4. lemma OAI.Release061.complexRealEquiv_symm_re line 52
  5. lemma OAI.Release061.complexRealEquiv_symm_im line 55
  6. lemma OAI.Release061.isSemialgebraic_real_image line 58
  7. lemma OAI.Release061.isSemialgebraic_of_real_image line 72
  8. lemma OAI.Release061.IsSemialgebraic.closure line 79
  9. lemma OAI.Release061.IsSemialgebraic.inter line 86
  10. lemma OAI.Release061.IsSemialgebraic.diff line 92
  11. lemma OAI.Release061.IsSemialgebraic.interior line 96
  12. lemma OAI.Release061.IsSemialgebraic.frontier line 101
  13. lemma OAI.Release061.SemialgebraicOn.coordinate_graph line 105
  14. def OAI.Release061.NashPatch.complexMap line 125
  15. lemma OAI.Release061.NashPatch.analytic_complexMap line 128
  16. lemma OAI.Release061.NashPatch.injective_fderiv_complexMap line 132
  17. lemma OAI.Release061.NashPatch.semialgebraic_complexMap_re line 140
  18. lemma OAI.Release061.NashPatch.semialgebraic_complexMap_im line 145
  19. theorem OAI.Release061.isSemialgebraic_finite_nash_cover line 152
  20. theorem OAI.Release061.semialgebraic_boundary_finite_nash_cover line 170