OAI/CategoryTheory/Thomason/SimplexBoxes.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

Simplex Boxes.

  1. def OAI.Thomason.GeometricRecognition.SimplexGeometry.chartBody line 15
  2. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.chartBody_closed line 18
  3. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.chartBody_convex line 25
  4. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.chartBody_bounded line 34
  5. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.strict_subset_interior_chartBody line 40
  6. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.chartBody_interior_nonempty line 51
  7. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.isOpenMap_sum line 60
  8. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.interior_chartBody line 74
  9. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.mem_frontier_chartBody line 87
  10. abbrev OAI.Thomason.GeometricRecognition.SimplexGeometry.cubeBody line 99
  11. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.interior_cubeBody line 101
  12. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.cubeBody_interior_nonempty line 116
  13. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.mem_frontier_cubeBody line 121
  14. def OAI.Thomason.GeometricRecognition.SimplexGeometry.simplexChartHomeomorph line 133
  15. def OAI.Thomason.GeometricRecognition.SimplexGeometry.cubeBodyHomeomorph line 173
  16. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.exists_chart_cube line 182
  17. def OAI.Thomason.GeometricRecognition.SimplexGeometry.chartCubeAmbient line 192
  18. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.chartCubeAmbient_spec line 195
  19. def OAI.Thomason.GeometricRecognition.SimplexGeometry.simplexCubeHomeomorph line 200
  20. lemma OAI.Thomason.GeometricRecognition.SimplexGeometry.simplexCubeHomeomorph_boundary line 204
  21. abbrev OAI.Thomason.GeometricRecognition.simplexVertices line 255
  22. abbrev OAI.Thomason.GeometricRecognition.simplexPoset line 256
  23. def OAI.Thomason.GeometricRecognition.simplexBoundary line 257
  24. def OAI.Thomason.GeometricRecognition.simplexPolyCoordinates line 259
  25. def OAI.Thomason.GeometricRecognition.simplexVertexOrder line 271
  26. lemma OAI.Thomason.GeometricRecognition.continuous_simplexPolyCoordinates line 274
  27. def OAI.Thomason.GeometricRecognition.simplexPolyHomeomorph line 278
  28. lemma OAI.Thomason.GeometricRecognition.simplex_subdivide_boundary line 293
  29. def OAI.Thomason.GeometricRecognition.simplexCubicalPair line 319
  30. abbrev OAI.Thomason.GeometricRecognition.orderedBoundary line 337
  31. lemma OAI.Thomason.GeometricRecognition.mem_orderedBoundary line 339
  32. lemma OAI.Thomason.GeometricRecognition.allowed_orderedBoundary line 369
  33. def OAI.Thomason.GeometricRecognition.boundaryFaceOrderIso line 384
  34. def OAI.Thomason.GeometricRecognition.sdBoundaryFacesIso line 402
  35. lemma OAI.Thomason.GeometricRecognition.sd_boundary_square line 408
  36. def OAI.Thomason.GeometricRecognition.simplexPairProjection line 414
  37. def OAI.Thomason.GeometricRecognition.simplexBoundaryProjection line 416
  38. lemma OAI.Thomason.GeometricRecognition.simplex_pair_square line 419
  39. lemma OAI.Thomason.GeometricRecognition.simplexPairProjection_local line 428
  40. lemma OAI.Thomason.GeometricRecognition.simplexBoundaryProjection_local line 430
  41. instance OAI.Thomason.GeometricRecognition.simplexBoundaryInclusion_mono line 433
  42. theorem OAI.Thomason.GeometricRecognition.weak_simplex_injective line 448
  43. theorem OAI.Thomason.GeometricRecognition.weak_simplex_surjective line 472
  44. def OAI.Thomason.GeometricRecognition.boxBoundary line 511
  45. lemma OAI.Thomason.GeometricRecognition.mem_boxBoundary line 517
  46. lemma OAI.Thomason.GeometricRecognition.allowed_boxBoundary line 533
  47. def OAI.Thomason.GeometricRecognition.boxBoundaryFaceIso line 548
  48. def OAI.Thomason.GeometricRecognition.sdBoxBoundaryIso line 556
  49. lemma OAI.Thomason.GeometricRecognition.sd_box_boundary_square line 562
  50. def OAI.Thomason.GeometricRecognition.boxPairProjection line 567
  51. def OAI.Thomason.GeometricRecognition.boxBoundaryProjection line 569
  52. lemma OAI.Thomason.GeometricRecognition.box_pair_square line 573
  53. lemma OAI.Thomason.GeometricRecognition.boxPairProjection_local line 582
  54. lemma OAI.Thomason.GeometricRecognition.boxBoundaryProjection_local line 584
  55. instance OAI.Thomason.GeometricRecognition.boxBoundaryInclusion_mono line 587
  56. def OAI.Thomason.GeometricRecognition.finiteBoxPair line 591
  57. def OAI.Thomason.GeometricRecognition.bit line 627
  58. def OAI.Thomason.GeometricRecognition.pack line 635
  59. lemma OAI.Thomason.GeometricRecognition.some_mem_pack line 638
  60. lemma OAI.Thomason.GeometricRecognition.none_mem_pack line 644
  61. def OAI.Thomason.GeometricRecognition.packOrder line 649
  62. lemma OAI.Thomason.GeometricRecognition.eraseNone_pack line 663
  63. lemma OAI.Thomason.GeometricRecognition.bit_pack line 668
  64. lemma OAI.Thomason.GeometricRecognition.pack_eraseNone_bit line 674
  65. def OAI.Thomason.GeometricRecognition.simplexOrder line 685
  66. def OAI.Thomason.GeometricRecognition.boxToPrism line 689
  67. def OAI.Thomason.GeometricRecognition.prismToBox line 700
  68. def OAI.Thomason.GeometricRecognition.boxPrismIso line 707
  69. lemma OAI.Thomason.GeometricRecognition.prismToBox_side_mem line 728
  70. lemma OAI.Thomason.GeometricRecognition.prismToBox_end_mem line 740
  71. def OAI.Thomason.GeometricRecognition.prismBoxSide line 755
  72. def OAI.Thomason.GeometricRecognition.prismBoxEnd line 760
  73. lemma OAI.Thomason.GeometricRecognition.prismBoxSide_comp line 765
  74. lemma OAI.Thomason.GeometricRecognition.prismBoxEnd_zero_comp line 768
  75. lemma OAI.Thomason.GeometricRecognition.prismBoxEnd_one_comp line 770
  76. lemma OAI.Thomason.GeometricRecognition.boxPrism_boundary_const line 773