OAI/CategoryTheory/Thomason/SimplicialApproximation.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Simplicial Approximation.

  1. def OAI.Thomason.GeometricRecognition.PolyPoint.vertex line 18
  2. lemma OAI.Thomason.GeometricRecognition.PolyPoint.vertex_weights line 24
  3. lemma OAI.Thomason.GeometricRecognition.PolyPoint.vertex_support line 27
  4. lemma OAI.Thomason.GeometricRecognition.PolyPoint.barycenter_support line 30
  5. def OAI.Thomason.GeometricRecognition.PolyPoint.PreservesChains line 39
  6. lemma OAI.Thomason.GeometricRecognition.PolyPoint.preservesChains_monotone line 42
  7. def OAI.Thomason.GeometricRecognition.PolyPoint.map line 50
  8. lemma OAI.Thomason.GeometricRecognition.PolyPoint.map_support line 66
  9. lemma OAI.Thomason.GeometricRecognition.PolyPoint.map_apply line 69
  10. lemma OAI.Thomason.GeometricRecognition.PolyPoint.continuous_map line 73
  11. lemma OAI.Thomason.GeometricRecognition.PolyPoint.map_vertex line 97
  12. def OAI.Thomason.GeometricRecognition.PolyPoint.segment line 102
  13. lemma OAI.Thomason.GeometricRecognition.PolyPoint.segment_zero line 125
  14. lemma OAI.Thomason.GeometricRecognition.PolyPoint.segment_one line 129
  15. lemma OAI.Thomason.GeometricRecognition.PolyPoint.segment_support line 133
  16. lemma OAI.Thomason.GeometricRecognition.PolyPoint.segment_self line 140
  17. lemma OAI.Thomason.GeometricRecognition.PolyPoint.exists_greatest line 146
  18. def OAI.Thomason.GeometricRecognition.PolyPoint.greatest line 154
  19. lemma OAI.Thomason.GeometricRecognition.PolyPoint.greatest_mem line 156
  20. lemma OAI.Thomason.GeometricRecognition.PolyPoint.le_greatest line 159
  21. lemma OAI.Thomason.GeometricRecognition.PolyPoint.greatest_mono line 162
  22. def OAI.Thomason.GeometricRecognition.PolyPoint.imageChain line 165
  23. def OAI.Thomason.GeometricRecognition.PolyPoint.orientedMap line 171
  24. lemma OAI.Thomason.GeometricRecognition.PolyPoint.orientedMap_mem line 175
  25. lemma OAI.Thomason.GeometricRecognition.PolyPoint.oriented_support line 180
  26. def OAI.Thomason.GeometricRecognition.PolyPoint.carrierHomotopy line 193
  27. lemma OAI.Thomason.GeometricRecognition.PolyPoint.carrierHomotopy_fixed line 215
  28. lemma OAI.Thomason.GeometricRecognition.PolyPoint.eq_vertex_of_support_subset line 224
  29. def OAI.Thomason.GeometricRecognition.Approximation.coordinateVertex line 255
  30. lemma OAI.Thomason.GeometricRecognition.Approximation.evaluate_coordinates line 257
  31. lemma OAI.Thomason.GeometricRecognition.Approximation.evaluate_vertex line 265
  32. lemma OAI.Thomason.GeometricRecognition.Approximation.norm_coordinateVertex_le line 270
  33. lemma OAI.Thomason.GeometricRecognition.Approximation.bound_coordinates line 276
  34. lemma OAI.Thomason.GeometricRecognition.Approximation.coordinate_level line 280
  35. lemma OAI.Thomason.GeometricRecognition.Approximation.coordinate_level_vertex line 285
  36. theorem OAI.Thomason.GeometricRecognition.Approximation.exists_star_labels line 289
  37. lemma OAI.Thomason.GeometricRecognition.Approximation.labels_preserve_chains line 321
  38. theorem OAI.Thomason.GeometricRecognition.Approximation.exists_oriented_approximation line 333
  39. def OAI.Thomason.GeometricRecognition.Approximation.affineMap line 345
  40. theorem OAI.Thomason.GeometricRecognition.Approximation.relative_approximation line 349
  41. structure OAI.Thomason.GeometricRecognition.Contiguity.ChainMap line 386
  42. instance OAI.Thomason.GeometricRecognition.Contiguity.(instance at line 389) line 389
  43. def OAI.Thomason.GeometricRecognition.Contiguity.Contiguous line 391
  44. def OAI.Thomason.GeometricRecognition.Contiguity.Related line 395
  45. def OAI.Thomason.GeometricRecognition.Contiguity.chainMapSetoid line 397
  46. lemma OAI.Thomason.GeometricRecognition.Contiguity.contiguous_of_carrier line 403
  47. theorem OAI.Thomason.GeometricRecognition.Contiguity.homotopy_star_labels line 418
  48. theorem OAI.Thomason.GeometricRecognition.Contiguity.homotopy_contiguity line 454
  49. def OAI.Thomason.GeometricRecognition.Contiguity.last line 482
  50. lemma OAI.Thomason.GeometricRecognition.Contiguity.last_support line 486
  51. lemma OAI.Thomason.GeometricRecognition.Contiguity.map_support_image line 497
  52. def OAI.Thomason.GeometricRecognition.Contiguity.toChainMap line 514
  53. theorem OAI.Thomason.GeometricRecognition.Contiguity.homotopy_subdivision_contiguity line 516
  54. def OAI.Thomason.GeometricRecognition.Contiguity.unionChain line 549
  55. def OAI.Thomason.GeometricRecognition.Contiguity.upperMap line 555
  56. lemma OAI.Thomason.GeometricRecognition.Contiguity.left_le_upper line 560
  57. lemma OAI.Thomason.GeometricRecognition.Contiguity.right_le_upper line 564
  58. lemma OAI.Thomason.GeometricRecognition.Contiguity.contiguous_nerve line 569
  59. lemma OAI.Thomason.GeometricRecognition.Contiguity.related_nerve line 579
  60. lemma OAI.Thomason.GeometricRecognition.Contiguity.orientedMap_monotone line 589
  61. theorem OAI.Thomason.GeometricRecognition.Contiguity.geometric_homotopy_detected line 598
  62. lemma OAI.Thomason.TopologicalHorn.anodyne_realization_retract line 625
  63. lemma OAI.Thomason.GeometricRecognition.homotopic_sections line 678
  64. lemma OAI.Thomason.GeometricRecognition.realization_endpoints_homotopic line 687
  65. lemma OAI.Thomason.GeometricRecognition.realization_homotopic line 701
  66. lemma OAI.Thomason.GeometricRecognition.adjunct_homotopic line 722
  67. lemma OAI.Thomason.GeometricRecognition.local_realization_heq line 729