OAI/CategoryTheory/Thomason/CubicalGeometry.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

Cubical Geometry.

  1. lemma OAI.Thomason.GeometricRecognition.realization_homotopy_rel line 16
  2. lemma OAI.Thomason.GeometricRecognition.based_homotopy_boundary line 79
  3. lemma OAI.Thomason.GeometricRecognition.based_related_boundary line 88
  4. lemma OAI.Thomason.GeometricRecognition.based_related_homotopy line 96
  5. lemma OAI.Thomason.GeometricRecognition.based_related_pre line 109
  6. lemma OAI.Thomason.GeometricRecognition.based_related_post line 119
  7. lemma OAI.Thomason.GeometricRecognition.pair_relative_nerve_detection line 128
  8. lemma OAI.Thomason.GeometricRecognition.pair_relative_nerve_descent line 168
  9. lemma OAI.Thomason.GeometricRecognition.map_eval line 216
  10. lemma OAI.Thomason.GeometricRecognition.nerveMap_realizeSimplex line 223
  11. lemma OAI.Thomason.GeometricRecognition.nerveRealizationHomeomorph_natural line 236
  12. def OAI.Thomason.GeometricRecognition.realizeMap line 260
  13. lemma OAI.Thomason.GeometricRecognition.realizeMap_comp line 263
  14. lemma OAI.Thomason.GeometricRecognition.cancel_geometric_homotopy line 269
  15. lemma OAI.Thomason.GeometricRecognition.geometric_homotopy_to_affine line 282
  16. theorem OAI.Thomason.GeometricRecognition.finite_order_geometric_faithful line 299
  17. def OAI.Thomason.GeometricRecognition.Cubical.chain line 349
  18. def OAI.Thomason.GeometricRecognition.Cubical.allFacesEquiv line 352
  19. lemma OAI.Thomason.GeometricRecognition.Cubical.sum_faces line 368
  20. def OAI.Thomason.GeometricRecognition.Cubical.compress line 373
  21. lemma OAI.Thomason.GeometricRecognition.Cubical.compress_apply line 376
  22. lemma OAI.Thomason.GeometricRecognition.Cubical.card_pos line 380
  23. lemma OAI.Thomason.GeometricRecognition.Cubical.compress_mem_support line 383
  24. def OAI.Thomason.GeometricRecognition.Cubical.coordinate line 388
  25. lemma OAI.Thomason.GeometricRecognition.Cubical.compress_evaluate line 391
  26. lemma OAI.Thomason.GeometricRecognition.Cubical.compress_nonneg line 403
  27. lemma OAI.Thomason.GeometricRecognition.Cubical.compress_chain line 406
  28. lemma OAI.Thomason.GeometricRecognition.Cubical.sum_weights line 413
  29. lemma OAI.Thomason.GeometricRecognition.Cubical.coordinate_nonneg line 416
  30. lemma OAI.Thomason.GeometricRecognition.Cubical.coordinate_le_sum line 422
  31. def OAI.Thomason.GeometricRecognition.Cubical.evaluate line 428
  32. lemma OAI.Thomason.GeometricRecognition.Cubical.continuous_evaluate line 432
  33. lemma OAI.Thomason.GeometricRecognition.Cubical.evaluate_injective line 443
  34. def OAI.Thomason.GeometricRecognition.Cubical.uncompress line 468
  35. lemma OAI.Thomason.GeometricRecognition.Cubical.uncompress_empty line 472
  36. lemma OAI.Thomason.GeometricRecognition.Cubical.uncompress_nonempty line 475
  37. lemma OAI.Thomason.GeometricRecognition.Cubical.compress_uncompress line 480
  38. lemma OAI.Thomason.GeometricRecognition.Cubical.uncompress_nonneg line 488
  39. lemma OAI.Thomason.GeometricRecognition.Cubical.uncompress_support_nonempty line 496
  40. lemma OAI.Thomason.GeometricRecognition.Cubical.uncompress_chain line 502
  41. lemma OAI.Thomason.GeometricRecognition.Cubical.sum_le_one_of_coordinates line 516
  42. lemma OAI.Thomason.GeometricRecognition.Cubical.coordinate_add line 543
  43. lemma OAI.Thomason.GeometricRecognition.Cubical.coordinate_empty line 550
  44. lemma OAI.Thomason.GeometricRecognition.Cubical.evaluate_surjective line 561
  45. def OAI.Thomason.GeometricRecognition.Cubical.cubeHomeomorph line 608
  46. lemma OAI.Thomason.GeometricRecognition.Cubical.coordinate_eq_zero_iff line 626
  47. lemma OAI.Thomason.GeometricRecognition.Cubical.coordinate_eq_one_iff line 641
  48. def OAI.Thomason.GeometricRecognition.Cubical.boundaryFaces line 666
  49. lemma OAI.Thomason.GeometricRecognition.Cubical.boundaryFaces_downward line 670
  50. lemma OAI.Thomason.GeometricRecognition.Cubical.subdivide_support line 676
  51. lemma OAI.Thomason.GeometricRecognition.Cubical.cube_boundary_iff line 680
  52. lemma OAI.Thomason.GeometricRecognition.Cubical.face_vertex_boundary line 696
  53. lemma OAI.Thomason.GeometricRecognition.Cubical.subdivided_cube_boundary_iff line 705
  54. def OAI.Thomason.GeometricRecognition.Cubical.pairCubeHomeomorph line 738
  55. def OAI.Thomason.GeometricRecognition.Cubical.boundaryEvaluate line 741
  56. lemma OAI.Thomason.GeometricRecognition.Cubical.boundaryEvaluate_injective line 746
  57. lemma OAI.Thomason.GeometricRecognition.Cubical.boundaryEvaluate_surjective line 752
  58. lemma OAI.Thomason.GeometricRecognition.Cubical.continuous_boundaryEvaluate line 767
  59. def OAI.Thomason.GeometricRecognition.Cubical.boundaryHomeomorph line 771
  60. lemma OAI.Thomason.GeometricRecognition.Cubical.boundaryHomeomorph_natural line 776