OAI/CategoryTheory/Thomason/RelativeContiguity.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Relative Contiguity.

  1. lemma OAI.Thomason.GeometricRecognition.nerveOrderMap_id line 16
  2. lemma OAI.Thomason.GeometricRecognition.nerveOrderMap_comp line 25
  3. lemma OAI.Thomason.GeometricRecognition.chainLast_local line 36
  4. lemma OAI.Thomason.GeometricRecognition.last_local line 42
  5. lemma OAI.Thomason.GeometricRecognition.orderMap_of_nerve line 59
  6. lemma OAI.Thomason.GeometricRecognition.stage_unmate line 65
  7. lemma OAI.Thomason.GeometricRecognition.finite_stage_order_representative line 83
  8. lemma OAI.Thomason.GeometricRecognition.finite_order_representative line 119
  9. lemma OAI.Thomason.GeometricRecognition.kan_poset_replacement_heq line 142
  10. def OAI.Thomason.GeometricRecognition.PolyPoint.restrict line 163
  11. def OAI.Thomason.GeometricRecognition.PolyPoint.inclusion line 176
  12. lemma OAI.Thomason.GeometricRecognition.PolyPoint.map_subtype_restrict line 178
  13. lemma OAI.Thomason.GeometricRecognition.PolyPoint.map_injective line 190
  14. lemma OAI.Thomason.GeometricRecognition.PolyPoint.map_subtype_support line 195
  15. lemma OAI.Thomason.GeometricRecognition.PolyPoint.exists_of_support line 202
  16. lemma OAI.Thomason.GeometricRecognition.chains_map_injective line 221
  17. lemma OAI.Thomason.GeometricRecognition.greatest_map line 229
  18. def OAI.Thomason.GeometricRecognition.levelMap line 238
  19. lemma OAI.Thomason.GeometricRecognition.levelMap_injective line 243
  20. lemma OAI.Thomason.GeometricRecognition.last_natural line 249
  21. lemma OAI.Thomason.GeometricRecognition.map_barycenter line 259
  22. lemma OAI.Thomason.GeometricRecognition.barycentricLinear_natural line 269
  23. lemma OAI.Thomason.GeometricRecognition.subdivide_natural line 283
  24. lemma OAI.Thomason.GeometricRecognition.levelHomeomorph_natural line 290
  25. lemma OAI.Thomason.GeometricRecognition.last_affine_support line 313
  26. def OAI.Thomason.GeometricRecognition.lastBarycentricHomotopy line 320
  27. lemma OAI.Thomason.GeometricRecognition.lastBarycentricHomotopy_support line 331
  28. lemma OAI.Thomason.GeometricRecognition.lastBarycentricHomotopy_pair line 343
  29. lemma OAI.Thomason.GeometricRecognition.kan_square_relative_surjective line 365
  30. lemma OAI.Thomason.GeometricRecognition.pre_fibration line 406
  31. lemma OAI.Thomason.GeometricRecognition.path_const_natural line 412
  32. lemma OAI.Thomason.GeometricRecognition.endsMap_comp line 418
  33. lemma OAI.Thomason.GeometricRecognition.endsInclusion_comp line 426
  34. lemma OAI.Thomason.GeometricRecognition.kan_square_relative_injective line 430
  35. def OAI.Thomason.GeometricRecognition.Contiguity.Fixed line 501
  36. def OAI.Thomason.GeometricRecognition.Contiguity.FixedMap line 503
  37. def OAI.Thomason.GeometricRecognition.Contiguity.FixedContiguous line 504
  38. def OAI.Thomason.GeometricRecognition.Contiguity.fixedMapSetoid line 507
  39. def OAI.Thomason.GeometricRecognition.Contiguity.RelativeRelated line 512
  40. lemma OAI.Thomason.GeometricRecognition.Contiguity.fixed_of_carrier line 516
  41. def OAI.Thomason.GeometricRecognition.Contiguity.relativeVertices line 524
  42. theorem OAI.Thomason.GeometricRecognition.Contiguity.homotopy_relative_contiguity line 527
  43. theorem OAI.Thomason.GeometricRecognition.Contiguity.homotopy_relative_subdivision_contiguity line 560
  44. def OAI.Thomason.GeometricRecognition.Contiguity.relativeFaceSet line 596
  45. def OAI.Thomason.GeometricRecognition.Contiguity.relativeFaceInclusion line 598
  46. lemma OAI.Thomason.GeometricRecognition.Contiguity.oriented_fixed line 601
  47. lemma OAI.Thomason.GeometricRecognition.Contiguity.upper_fixed line 606
  48. def OAI.Thomason.GeometricRecognition.Contiguity.constantOrder line 615
  49. def OAI.Thomason.GeometricRecognition.Contiguity.BasedHomotopy line 617
  50. def OAI.Thomason.GeometricRecognition.Contiguity.BasedRelated line 620
  51. lemma OAI.Thomason.GeometricRecognition.Contiguity.orderHomotopy_fixed line 623
  52. lemma OAI.Thomason.GeometricRecognition.Contiguity.fixed_contiguous_nerve line 637
  53. lemma OAI.Thomason.GeometricRecognition.Contiguity.fixed_related_nerve line 654
  54. lemma OAI.Thomason.GeometricRecognition.Contiguity.relative_related_nerve line 666
  55. lemma OAI.Thomason.GeometricRecognition.uncurry_homotopy_restriction line 685
  56. lemma OAI.Thomason.GeometricRecognition.curry_homotopy_restriction line 700
  57. lemma OAI.Thomason.GeometricRecognition.pair_local_surjective line 713
  58. lemma OAI.Thomason.GeometricRecognition.pair_local_injective line 741