OAI/CategoryTheory/Thomason/FiberRecognition.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Fiber Recognition.

  1. theorem OAI.Thomason.GeometricRecognition.weak_box_injective line 16
  2. theorem OAI.Thomason.GeometricRecognition.weak_box_surjective line 41
  3. lemma OAI.Thomason.GeometricRecognition.zero_face_horn_iff line 79
  4. def OAI.Thomason.GeometricRecognition.boundaryInHorn line 100
  5. def OAI.Thomason.GeometricRecognition.hornInBoundary line 106
  6. lemma OAI.Thomason.GeometricRecognition.boundaryInHorn_ι line 112
  7. lemma OAI.Thomason.GeometricRecognition.hornInBoundary_ι line 115
  8. lemma OAI.Thomason.GeometricRecognition.boundaryInHorn_square line 117
  9. instance OAI.Thomason.GeometricRecognition.(instance at line 121) line 121
  10. lemma OAI.Thomason.GeometricRecognition.boundary_horn_isPushout line 124
  11. lemma OAI.Thomason.GeometricRecognition.simplex_homotopic_const line 172
  12. lemma OAI.Thomason.GeometricRecognition.straighten_boundary line 187
  13. lemma OAI.Thomason.GeometricRecognition.nullhomotopy_boundary_of_face line 199
  14. theorem OAI.Thomason.GeometricRecognition.terminal_rlp_of_nullsimplices line 233
  15. lemma OAI.Thomason.GeometricRecognition.based_homotopy_zero line 258
  16. theorem OAI.Thomason.GeometricRecognition.weak_terminal_rlp line 265
  17. lemma OAI.Thomason.GeometricRecognition.correct_nullhomotopy_to_fiber line 301
  18. lemma OAI.Thomason.GeometricRecognition.correct_box_nullhomotopy line 367
  19. lemma OAI.Thomason.GeometricRecognition.weak_fibration_box_nullhomotopy line 413
  20. def OAI.Thomason.GeometricRecognition.strictFiber line 440
  21. lemma OAI.Thomason.GeometricRecognition.strictFiber_ι_comp line 448
  22. def OAI.Thomason.GeometricRecognition.strictFiberLift line 453
  23. lemma OAI.Thomason.GeometricRecognition.strictFiberLift_ι line 463
  24. lemma OAI.Thomason.GeometricRecognition.strictFiber_kan line 467
  25. lemma OAI.Thomason.GeometricRecognition.strictFiber_homotopy line 484
  26. lemma OAI.Thomason.GeometricRecognition.weak_fibration_vertex_homotopy line 504
  27. lemma OAI.Thomason.GeometricRecognition.strictFiber_vertex_iff line 531
  28. lemma OAI.Thomason.GeometricRecognition.strictFiber_vertex_homotopy line 542
  29. lemma OAI.Thomason.GeometricRecognition.cubical_null_of_group_subsingleton line 567
  30. lemma OAI.Thomason.GeometricRecognition.cube_classes_subsingleton_of_boxes line 592
  31. theorem OAI.Thomason.GeometricRecognition.terminal_rlp_of_nullboxes line 618
  32. lemma OAI.Thomason.GeometricRecognition.strictFiber_based_box_null line 661
  33. theorem OAI.Thomason.GeometricRecognition.weak_kan_fibration_fiber_rlp line 685
  34. def OAI.Thomason.GeometricRecognition.simplexConeOrder line 708
  35. def OAI.Thomason.GeometricRecognition.simplexCone line 721
  36. lemma OAI.Thomason.GeometricRecognition.simplexCone_zero line 728
  37. lemma OAI.Thomason.GeometricRecognition.simplexCone_one line 734
  38. theorem OAI.Thomason.GeometricRecognition.fibration_rlp_of_fibers line 740