OAI/Geometry/HyperbolicGroups/FinitePolyhedron.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Literal barycentric realizations of finite abstract complexes. No abstract CW or homotopy replacement is used in the definitions.

  1. def OAI.HyperbolicObstruction.FinitePolyhedron.simplex line 15
  2. def OAI.HyperbolicObstruction.FinitePolyhedron.carrierSet line 18
  3. abbrev OAI.HyperbolicObstruction.FinitePolyhedron.Carrier line 22
  4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.simplex_convex line 24
  5. lemma OAI.HyperbolicObstruction.FinitePolyhedron.simplex_closed line 32
  6. lemma OAI.HyperbolicObstruction.FinitePolyhedron.simplex_compact line 46
  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.carrierSet_eq_union line 56
  8. lemma OAI.HyperbolicObstruction.FinitePolyhedron.carrierSet_compact line 63
  9. instance OAI.HyperbolicObstruction.FinitePolyhedron.(instance at line 67) line 67
  10. def OAI.HyperbolicObstruction.FinitePolyhedron.vertex line 70
  11. lemma OAI.HyperbolicObstruction.FinitePolyhedron.vertex_mem_simplex line 82
  12. lemma OAI.HyperbolicObstruction.FinitePolyhedron.simplex_subset_carrier line 89
  13. lemma OAI.HyperbolicObstruction.FinitePolyhedron.joined_of_simplex line 93
  14. lemma OAI.HyperbolicObstruction.FinitePolyhedron.vertex_joined_of_edge line 98
  15. lemma OAI.HyperbolicObstruction.FinitePolyhedron.exists_joined_vertex line 102
  16. lemma OAI.HyperbolicObstruction.FinitePolyhedron.pathConnected_of_vertex_connected line 108