OAI/Geometry/HyperbolicGroups/EdgeCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Literal equality tests for barycentric edges. These prevent arbitrary choices of edge homotopies from being silently identified at intersections.

  1. lemma OAI.HyperbolicObstruction.FinitePolyhedron.vertex_injective line 14
  2. lemma OAI.HyperbolicObstruction.FinitePolyhedron.edgePath_coordinate line 20
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.edgePath_eq_vertex_cases line 25
  4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.edgePath_eq_edge_interior line 50