OAI/Geometry/HypersurfaceGerms/RootPages.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Homeomorphic inner-root models and naturality of the root-to-base projection.

  1. abbrev OAI.AmbientMultiplicity.SourceInnerPage.Base line 15
  2. def OAI.AmbientMultiplicity.SourceInnerPage.sourceH line 18
  3. lemma OAI.AmbientMultiplicity.SourceInnerPage.continuous_sourceH line 20
  4. def OAI.AmbientMultiplicity.SourceInnerPage.low0 line 24
  5. def OAI.AmbientMultiplicity.SourceInnerPage.low1 line 25
  6. lemma OAI.AmbientMultiplicity.SourceInnerPage.low0_analytic line 27
  7. lemma OAI.AmbientMultiplicity.SourceInnerPage.low1_analytic line 32
  8. def OAI.AmbientMultiplicity.SourceInnerPage.R0 line 38
  9. def OAI.AmbientMultiplicity.SourceInnerPage.R1 line 39
  10. lemma OAI.AmbientMultiplicity.SourceInnerPage.R0_eq_source line 41
  11. lemma OAI.AmbientMultiplicity.SourceInnerPage.R1_eq_source line 48
  12. lemma OAI.AmbientMultiplicity.SourceInnerPage.common_base_cut line 55
  13. abbrev OAI.AmbientMultiplicity.SourceInnerPage.BasePage line 78
  14. instance OAI.AmbientMultiplicity.SourceInnerPage.basePage_compact line 81
  15. abbrev OAI.AmbientMultiplicity.SourceInnerPage.Disk line 92
  16. abbrev OAI.AmbientMultiplicity.SourceInnerPage.RootBase line 93
  17. def OAI.AmbientMultiplicity.SourceInnerPage.onRootBase line 95
  18. abbrev OAI.AmbientMultiplicity.SourceInnerPage.Model line 100
  19. lemma OAI.AmbientMultiplicity.SourceInnerPage.y_bound_eq line 106
  20. lemma OAI.AmbientMultiplicity.SourceInnerPage.z_bound_eq line 116
  21. def OAI.AmbientMultiplicity.SourceInnerPage.weightedModelHomeomorph line 129
  22. lemma OAI.AmbientMultiplicity.SourceInnerPage.continuous_onRootBase_rescaled line 137
  23. lemma OAI.AmbientMultiplicity.SourceInnerPage.eventually_bound_on_base line 149
  24. def OAI.AmbientMultiplicity.SourceInnerPage.modelCollapseHomotopyEquiv line 163
  25. theorem OAI.AmbientMultiplicity.SourceInnerPage.exact_inner_models line 186
  26. def OAI.AmbientMultiplicity.SourceInnerPage.pi0 line 209
  27. def OAI.AmbientMultiplicity.SourceInnerPage.pi1 line 210
  28. def OAI.AmbientMultiplicity.SourceInnerPage.d0 line 211
  29. def OAI.AmbientMultiplicity.SourceInnerPage.d1 line 212
  30. lemma OAI.AmbientMultiplicity.SourceInnerPage.continuous_pi0 line 214
  31. lemma OAI.AmbientMultiplicity.SourceInnerPage.continuous_pi1 line 215
  32. lemma OAI.AmbientMultiplicity.SourceInnerPage.low0_zero line 217
  33. lemma OAI.AmbientMultiplicity.SourceInnerPage.low1_zero line 223
  34. lemma OAI.AmbientMultiplicity.SourceInnerPage.root0_eq_quartic line 229
  35. lemma OAI.AmbientMultiplicity.SourceInnerPage.root1_eq_quartic line 233
  36. lemma OAI.AmbientMultiplicity.SourceInnerPage.eventually_root_graph line 238
  37. def OAI.AmbientMultiplicity.SourceInnerPage.join line 256
  38. lemma OAI.AmbientMultiplicity.SourceInnerPage.join_small line 258
  39. lemma OAI.AmbientMultiplicity.SourceInnerPage.base3_join line 267
  40. theorem OAI.AmbientMultiplicity.SourceInnerPage.common_root_chart line 273
  41. abbrev OAI.AmbientMultiplicity.SourceInnerPage.RootPage line 346
  42. abbrev OAI.AmbientMultiplicity.SourceInnerPage.GraphPage line 350
  43. lemma OAI.AmbientMultiplicity.SourceInnerPage.rootPage_unscaled_zero line 364
  44. lemma OAI.AmbientMultiplicity.SourceInnerPage.rootPage_unscaled_small line 373
  45. lemma OAI.AmbientMultiplicity.SourceInnerPage.rootPage_graph_eq line 378
  46. def OAI.AmbientMultiplicity.SourceInnerPage.rootToGraph line 385
  47. def OAI.AmbientMultiplicity.SourceInnerPage.graphToRoot line 398
  48. lemma OAI.AmbientMultiplicity.SourceInnerPage.graph_root_left_inverse line 412
  49. lemma OAI.AmbientMultiplicity.SourceInnerPage.root_graph_right_inverse line 425
  50. def OAI.AmbientMultiplicity.SourceInnerPage.rootGraphHomeomorph line 438
  51. theorem OAI.AmbientMultiplicity.SourceInnerPage.exact_root_pages line 466
  52. def OAI.AmbientMultiplicity.SourceInnerPage.graphPageProjection line 496
  53. def OAI.AmbientMultiplicity.SourceInnerPage.rootPageProjection line 503
  54. lemma OAI.AmbientMultiplicity.SourceInnerPage.rootGraphHomeomorph_over_base line 520
  55. lemma OAI.AmbientMultiplicity.SourceInnerPage.rootGraphHomeomorph_homology_over_base line 532
  56. def OAI.AmbientMultiplicity.SourceInnerPage.baseSection line 548
  57. def OAI.AmbientMultiplicity.SourceInnerPage.rootBaseHomotopyEquiv line 554
  58. def OAI.AmbientMultiplicity.SourceInnerPage.rootBaseHomologyIso line 586