OAI/CategoryTheory/Thomason/RelativeRepresentation.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Relative Representation.

  1. lemma OAI.Thomason.GeometricRecognition.pair_local_surjective_plain line 15
  2. lemma OAI.Thomason.GeometricRecognition.pair_local_injective_plain line 39
  3. lemma OAI.Thomason.GeometricRecognition.vertex_injective line 83
  4. lemma OAI.Thomason.GeometricRecognition.nerveOrderMap_mono line 90
  5. lemma OAI.Thomason.GeometricRecognition.pair_geometric_approximation line 98
  6. lemma OAI.Thomason.GeometricRecognition.descend_pair_approximation line 124
  7. lemma OAI.Thomason.GeometricRecognition.unmate_homotopy_relative line 150
  8. lemma OAI.Thomason.GeometricRecognition.stage_unmate_boundary line 216
  9. lemma OAI.Thomason.GeometricRecognition.stage_unmate_relative line 224
  10. lemma OAI.Thomason.GeometricRecognition.fill_rectangle_over line 275
  11. lemma OAI.Thomason.GeometricRecognition.fill_rectangle_relative_tensor line 296
  12. lemma OAI.Thomason.GeometricRecognition.fill_rectangle_relative line 316
  13. lemma OAI.Thomason.GeometricRecognition.based_homotopy_symm line 345
  14. lemma OAI.Thomason.GeometricRecognition.based_homotopy_trans line 356
  15. lemma OAI.Thomason.GeometricRecognition.based_homotopy_refl line 377
  16. lemma OAI.Thomason.GeometricRecognition.based_homotopy_pre line 383
  17. lemma OAI.Thomason.GeometricRecognition.based_homotopy_post line 392
  18. lemma OAI.Thomason.GeometricRecognition.constantOrder_comp line 400
  19. lemma OAI.Thomason.GeometricRecognition.nerve_constant_pre line 404
  20. lemma OAI.Thomason.GeometricRecognition.sdNerve_inv_natural line 410
  21. lemma OAI.Thomason.GeometricRecognition.sdNerve_inv_last line 420
  22. lemma OAI.Thomason.GeometricRecognition.chainLast_natural line 426
  23. structure OAI.Thomason.GeometricRecognition.PairRefinement line 438
  24. def OAI.Thomason.GeometricRecognition.PairRefinement.identity line 457
  25. def OAI.Thomason.GeometricRecognition.PairRefinement.prepend line 474
  26. lemma OAI.Thomason.GeometricRecognition.exSequence_zero_succ line 499
  27. lemma OAI.Thomason.GeometricRecognition.exSequence_zero_inclusion line 517
  28. lemma OAI.Thomason.GeometricRecognition.nerve_constant_pre' line 522
  29. lemma OAI.Thomason.GeometricRecognition.stage_order_pair_representative line 527
  30. lemma OAI.Thomason.GeometricRecognition.finite_pair_order_representative line 619
  31. lemma OAI.Thomason.GeometricRecognition.edge_homotopy_const line 660
  32. lemma OAI.Thomason.GeometricRecognition.component_homotopic_const line 668
  33. lemma OAI.Thomason.GeometricRecognition.homotopy_extension line 682
  34. lemma OAI.Thomason.GeometricRecognition.point_mono line 696
  35. lemma OAI.Thomason.GeometricRecognition.nerve_constant_vertex line 706
  36. lemma OAI.Thomason.GeometricRecognition.pointed_kan_poset_replacement line 712
  37. lemma OAI.Thomason.GeometricRecognition.pointed_kan_ex_replacement line 735