OAI/CategoryTheory/Thomason/Polyhedra.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

Polyhedra.

  1. structure OAI.Thomason.GeometricRecognition.PolyPoint line 13
  2. def OAI.Thomason.GeometricRecognition.PolyPoint.Face line 23
  3. instance OAI.Thomason.GeometricRecognition.PolyPoint.faceTopology line 25
  4. lemma OAI.Thomason.GeometricRecognition.PolyPoint.face_coords_injective line 28
  5. instance OAI.Thomason.GeometricRecognition.PolyPoint.faceT2 line 35
  6. structure OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex line 38
  7. instance OAI.Thomason.GeometricRecognition.PolyPoint.weakTopology line 43
  8. lemma OAI.Thomason.GeometricRecognition.PolyPoint.isClosed_iff_faces line 47
  9. lemma OAI.Thomason.GeometricRecognition.PolyPoint.isClosed_of_face_finite line 53
  10. theorem OAI.Thomason.GeometricRecognition.PolyPoint.compact_finite_carrier line 58
  11. lemma OAI.Thomason.GeometricRecognition.PolyPoint.continuous_chainFace_val line 106
  12. lemma OAI.Thomason.GeometricRecognition.PolyPoint.continuous_weights line 112
  13. instance OAI.Thomason.GeometricRecognition.PolyPoint.(instance at line 118) line 118
  14. def OAI.Thomason.GeometricRecognition.PolyPoint.evalWeights line 123
  15. lemma OAI.Thomason.GeometricRecognition.PolyPoint.evalWeights_support line 127
  16. def OAI.Thomason.GeometricRecognition.PolyPoint.eval line 141
  17. lemma OAI.Thomason.GeometricRecognition.PolyPoint.continuous_eval line 164
  18. lemma OAI.Thomason.GeometricRecognition.PolyPoint.evalWeights_map line 191
  19. lemma OAI.Thomason.GeometricRecognition.PolyPoint.eval_map line 198
  20. lemma OAI.Thomason.GeometricRecognition.PolyPoint.evalWeights_apply_image line 205
  21. instance OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.carrierLinearOrder line 214
  22. def OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.dimension line 218
  23. lemma OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.card_eq line 220
  24. def OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.enumerate line 226
  25. def OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.vertices line 229
  26. lemma OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.vertices_injective line 232
  27. lemma OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.vertices_mem line 235
  28. lemma OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.vertices_surjective line 238
  29. def OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.coordinates line 243
  30. lemma OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.continuous_coordinates line 257
  31. lemma OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.eval_coordinates line 263
  32. def OAI.Thomason.GeometricRecognition.PolyPoint.supportIndex line 281
  33. def OAI.Thomason.GeometricRecognition.polyCocone line 295
  34. def OAI.Thomason.GeometricRecognition.nerveRealizationIsColimit line 315
  35. def OAI.Thomason.GeometricRecognition.realizationToPoly line 319
  36. def OAI.Thomason.GeometricRecognition.realizeSimplex line 324
  37. lemma OAI.Thomason.GeometricRecognition.continuous_realizeSimplex line 329
  38. lemma OAI.Thomason.GeometricRecognition.realizeSimplex_map line 334
  39. def OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.inclusion line 364
  40. lemma OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.vertices_inclusion line 369
  41. lemma OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.eval_injective line 374
  42. lemma OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.map_coordinates line 383
  43. def OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.faceReal line 395
  44. lemma OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.continuous_faceReal line 398
  45. lemma OAI.Thomason.GeometricRecognition.PolyPoint.ChainIndex.faceReal_inclusion line 401
  46. def OAI.Thomason.GeometricRecognition.polyToRealization line 409
  47. lemma OAI.Thomason.GeometricRecognition.polyToRealization_face line 412
  48. lemma OAI.Thomason.GeometricRecognition.continuous_polyToRealization line 417
  49. def OAI.Thomason.GeometricRecognition.PolyPoint.imageIndex line 428
  50. def OAI.Thomason.GeometricRecognition.PolyPoint.imageOrdinal line 439
  51. lemma OAI.Thomason.GeometricRecognition.PolyPoint.image_vertices line 445
  52. lemma OAI.Thomason.GeometricRecognition.polyToRealization_eval line 452
  53. lemma OAI.Thomason.GeometricRecognition.realizationToPoly_realizeSimplex line 471
  54. lemma OAI.Thomason.GeometricRecognition.realizationToPoly_polyToRealization line 491
  55. def OAI.Thomason.GeometricRecognition.polyToRealizationHom line 497
  56. lemma OAI.Thomason.GeometricRecognition.realizationToPoly_comp_polyToRealization line 500
  57. lemma OAI.Thomason.GeometricRecognition.polyToRealization_realizationToPoly line 522
  58. def OAI.Thomason.GeometricRecognition.nerveRealizationHomeomorph line 526
  59. theorem OAI.Thomason.GeometricRecognition.nerve_compact_finite_carrier line 534
  60. def OAI.Thomason.GeometricRecognition.PolyPoint.barycenter line 552
  61. lemma OAI.Thomason.GeometricRecognition.PolyPoint.barycenter_apply line 573
  62. def OAI.Thomason.GeometricRecognition.PolyPoint.barycentricLinear line 578
  63. lemma OAI.Thomason.GeometricRecognition.PolyPoint.barycentricLinear_apply line 581
  64. lemma OAI.Thomason.GeometricRecognition.PolyPoint.barycentricLinear_total line 586
  65. lemma OAI.Thomason.GeometricRecognition.PolyPoint.barycentric_cone_step line 598
  66. lemma OAI.Thomason.GeometricRecognition.PolyPoint.exists_barycentric_decomposition line 641
  67. lemma OAI.Thomason.GeometricRecognition.PolyPoint.barycentricLinear_nonneg line 698
  68. lemma OAI.Thomason.GeometricRecognition.PolyPoint.barycentricLinear_support line 703
  69. lemma OAI.Thomason.GeometricRecognition.PolyPoint.flagCarrier_chain line 715
  70. def OAI.Thomason.GeometricRecognition.PolyPoint.subdivide line 726
  71. lemma OAI.Thomason.GeometricRecognition.PolyPoint.subdivide_surjective line 733
  72. lemma OAI.Thomason.GeometricRecognition.PolyPoint.continuous_subdivide line 741