OAI/Geometry/HyperbolicGroups/FinitePolyhedronPaths.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Canonical straight paths and the actual contractible open vertex stars. There are no combinatorial-to-topological equivalences assumed here.

  1. lemma OAI.HyperbolicObstruction.FinitePolyhedron.wideStar_vertex line 17
  2. lemma OAI.HyperbolicObstruction.FinitePolyhedron.openStar_ambient_starConvex line 27
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.vertex_mem_openStar line 32
  4. def OAI.HyperbolicObstruction.FinitePolyhedron.openStarHomeomorph line 35
  5. instance OAI.HyperbolicObstruction.FinitePolyhedron.openStar_contractible line 44
  6. def OAI.HyperbolicObstruction.FinitePolyhedron.straight line 51

    Source documentation

    The affine path when its entire segment lies in the actual carrier.

    def straight (x y : Carrier K) (h : segment ℝ x.val y.val ⊆ carrierSet K) : Path x y where
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Carrier, OAI.HyperbolicObstruction.FinitePolyhedron.carrierSet

  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.straight_val line 58
  8. lemma OAI.HyperbolicObstruction.FinitePolyhedron.straight_in_face line 62
  9. def OAI.HyperbolicObstruction.FinitePolyhedron.facePath line 67
  10. def OAI.HyperbolicObstruction.FinitePolyhedron.edgePath line 71
  11. def OAI.HyperbolicObstruction.FinitePolyhedron.starPath line 75

    Source documentation

    The radial path from a star-center to a point in its open star.

    def starPath (v : V) (x : Carrier K) (hx : x ∈ openStar K v) : Path (vertex K v) x :=
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Carrier, OAI.HyperbolicObstruction.FinitePolyhedron.openStar, OAI.HyperbolicObstruction.FinitePolyhedron.vertex

  12. lemma OAI.HyperbolicObstruction.FinitePolyhedron.starPath_mem line 78
  13. lemma OAI.HyperbolicObstruction.FinitePolyhedron.homotopic_in_star line 83