OAI/Geometry/SplitTangent/RationalFamilies.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Rational Families.

  1. abbrev OAI.AnalyticZeroCover.Space line 22
  2. structure OAI.AnalyticZeroCover.Patch line 25
  3. def OAI.AnalyticZeroCover.Patch.image line 33
  4. theorem OAI.AnalyticZeroCover.regular_zero_patchAlternative line 38
  5. lemma OAI.AnalyticZeroCover.vertical_eq_zero_of_rank_le line 129
  6. lemma OAI.AnalyticZeroCover.finrank_range_comp_le line 147
  7. lemma OAI.AnalyticZeroCover.Patch.dimH_image_le line 158
  8. lemma OAI.AnalyticZeroCover.constant_vertical line 179
  9. theorem OAI.AnalyticZeroCover.local_image_patchAlternative line 208
  10. instance OAI.SplitTangent.FormalCauchy.(instance at line 318) line 318
  11. lemma OAI.AnalyticZeroCover.eventually_zero_of_all_derivatives line 362
  12. lemma OAI.AnalyticZeroCover.analyticAt_iterated line 371
  13. def OAI.AnalyticZeroCover.coeffDerivative line 377
  14. lemma OAI.AnalyticZeroCover.coeffDerivative_analytic line 380
  15. lemma OAI.AnalyticZeroCover.derivative_zero_of_coefficients line 386
  16. theorem OAI.AnalyticZeroCover.exists_regular_derivative line 397
  17. theorem OAI.AnalyticZeroCover.regular_zero_patch line 447
  18. theorem OAI.AnalyticZeroCover.countable_regular_zero_cover line 529
  19. theorem OAI.AnalyticZeroCover.countable_zero_cover line 552
  20. theorem OAI.AnalyticZeroCover.countable_zero_cover_of_nonzero line 573
  21. structure OAI.AnalyticZeroCover.AnalyticSetOn line 595
  22. lemma OAI.AnalyticZeroCover.AnalyticSetOn.closure_interior line 603
  23. theorem OAI.AnalyticZeroCover.AnalyticSetOn.interior_eq_empty line 626
  24. lemma OAI.AnalyticZeroCover.AnalyticSetOn.local_cover line 638
  25. theorem OAI.AnalyticZeroCover.AnalyticSetOn.countable_lower_cover line 667
  26. def OAI.AnalyticZeroCover.Patch.comp line 696
  27. lemma OAI.AnalyticZeroCover.Patch.comp_image_subset line 705
  28. theorem OAI.AnalyticZeroCover.Patch.countable_accepted_cover line 713
  29. theorem OAI.AnalyticZeroCover.countable_open_patches line 759
  30. abbrev OAI.SplitTangent.RationalParameters.Coeff line 791
  31. def OAI.SplitTangent.RationalParameters.ev line 794
  32. lemma OAI.SplitTangent.RationalParameters.ev_analytic line 797
  33. lemma OAI.SplitTangent.RationalParameters.ev_continuous line 806
  34. lemma OAI.SplitTangent.RationalParameters.ev_transition line 810
  35. def OAI.SplitTangent.RationalParameters.regular line 823
  36. lemma OAI.SplitTangent.RationalParameters.isOpen_regular line 826
  37. lemma OAI.SplitTangent.RationalParameters.regular_nonzero line 841
  38. def OAI.SplitTangent.RationalParameters.accepted line 858
  39. def OAI.SplitTangent.RationalParameters.evaluation line 867
  40. lemma OAI.SplitTangent.RationalParameters.evaluation_holomorphicAt line 871
  41. lemma OAI.SplitTangent.RationalParameters.evaluation_overlap line 883
  42. def OAI.SplitTangent.RationalParameters.pairEvaluation line 888
  43. lemma OAI.SplitTangent.RationalParameters.pairEvaluation_holomorphicAt line 892
  44. def OAI.SplitTangent.RationalParameters.family line 903
  45. lemma OAI.SplitTangent.RationalParameters.analyticSetOn_incidence line 931
  46. theorem OAI.AnalyticZeroCover.local_image_patch line 1013
  47. def OAI.AnalyticZeroCover.pivot line 1108
  48. lemma OAI.AnalyticZeroCover.pivot_analytic line 1112
  49. lemma OAI.AnalyticZeroCover.pivot_surjective line 1130
  50. lemma OAI.AnalyticZeroCover.exists_pivot line 1146
  51. lemma OAI.AnalyticZeroCover.dimH_image_le_of_local line 1174
  52. theorem OAI.AnalyticZeroCover.rank_dimH_le line 1193
  53. lemma OAI.AnalyticZeroCover.finrank_range_lt_of_not_surjective line 1252
  54. lemma OAI.AnalyticZeroCover.rank_dimH_le_open line 1259
  55. theorem OAI.AnalyticZeroCover.exists_surjective_of_countable_cover line 1272
  56. theorem OAI.SplitTangent.exists_chart_submersion_of_cover line 1312
  57. lemma OAI.SplitTangent.surjective_mfderiv_of_chart line 1354
  58. lemma OAI.SplitTangent.eventually_surjective_fderiv line 1372
  59. theorem OAI.SplitTangent.RationalFamily.integrable_both_of_submersive line 1397