OAI/Geometry/HyperbolicGroups/EdgeChain.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.append line 15
2. def OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.path line 19
3. abbrev OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.pathClass line 23
4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.pathClass_nil line 26
5. lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.pathClass_cons line 27
6. lemma OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain.pathClass_append line 30
7. def OAI.HyperbolicObstruction.FinitePolyhedron.EdgeTame line 38

   Source documentation

   Normal form with one radial segment at each endpoint.

   def EdgeTame {x y : Carrier K} (p : Path.Homotopic.Quotient x y) : Prop :=
   …

   Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Carrier

8. lemma OAI.HyperbolicObstruction.FinitePolyhedron.edgeTame_of_star line 43
9. lemma OAI.HyperbolicObstruction.FinitePolyhedron.edgeTame_refl line 59
10. lemma OAI.HyperbolicObstruction.FinitePolyhedron.edgeTame_trans line 63
11. theorem OAI.HyperbolicObstruction.FinitePolyhedron.all_paths_edgeTame line 77
12. lemma OAI.HyperbolicObstruction.FinitePolyhedron.vertex_in_openStar line 83
13. lemma OAI.HyperbolicObstruction.FinitePolyhedron.starPath_self line 89
14. theorem OAI.HyperbolicObstruction.FinitePolyhedron.edgePath_representative line 98

    Source documentation

    Every actual continuous path between vertices has a finite edge-chain representative, with the same endpoints and in its actual homotopy class.

    theorem edgePath_representative {a b : V} (p : Path (vertex K a) (vertex K b)) :
        ∃ c : EdgeChain K a b, p.Homotopic c.path := by
    …

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.vertex, OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain