OAI/Geometry/HyperbolicGroups/FinitePolyhedronEdgePaths.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Edge paths generate the actual path homotopy groupoid of a finite barycentric realization. The proof uses the literal open stars, not an unproved simplicial-approximation principle.

  1. abbrev OAI.HyperbolicObstruction.FinitePolyhedron.inFace line 15
  2. def OAI.HyperbolicObstruction.FinitePolyhedron.inFaceHomeomorph line 17
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.inFace_contractible line 26
  4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.homotopic_in_face line 33
  5. lemma OAI.HyperbolicObstruction.FinitePolyhedron.straight_mem_face line 39
  6. lemma OAI.HyperbolicObstruction.FinitePolyhedron.positive_mem_face line 44
  7. lemma OAI.HyperbolicObstruction.FinitePolyhedron.commonStar_edge line 51
  8. lemma OAI.HyperbolicObstruction.FinitePolyhedron.radial_bridge line 58
  9. inductive OAI.HyperbolicObstruction.FinitePolyhedron.EdgeChain line 80

    Source documentation

    A genuine finite vertex edge path.

    inductive EdgeChain : V → V → Type _
  | nil (a) : EdgeChain a a
  | cons {a b c} (edge : {a,b} ∈ K.faces) (tail : EdgeChain b c) : EdgeChain a c

end HyperbolicObstruction.FinitePolyhedron
end

end OAI