OAI/Geometry/HyperbolicGroups/FinitePolyhedronLocal.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Finite barycentric carriers are strongly locally contractible. The contracting neighborhoods retain every positive coordinate of their center, so straight contraction never crosses a missing simplex.

  1. def OAI.HyperbolicObstruction.FinitePolyhedron.wideStar line 16
  2. lemma OAI.HyperbolicObstruction.FinitePolyhedron.wideStar_open line 19
  3. lemma OAI.HyperbolicObstruction.FinitePolyhedron.self_mem_wideStar line 29
  4. lemma OAI.HyperbolicObstruction.FinitePolyhedron.supported_on_face line 31
  5. lemma OAI.HyperbolicObstruction.FinitePolyhedron.wideStar_starConvex line 42
  6. def OAI.HyperbolicObstruction.FinitePolyhedron.smallStar line 59

    Source documentation

    Intersection of a straight-contraction star with an arbitrarily small ambient ball.

    def smallStar (x : Carrier K) (ε : ℝ) : Set (Carrier K) :=
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Carrier

  7. def OAI.HyperbolicObstruction.FinitePolyhedron.smallStarAmbient line 62
  8. lemma OAI.HyperbolicObstruction.FinitePolyhedron.smallStarAmbient_starConvex line 65
  9. lemma OAI.HyperbolicObstruction.FinitePolyhedron.smallStarAmbient_mem line 69
  10. def OAI.HyperbolicObstruction.FinitePolyhedron.smallStarHomeomorph line 74

    Source documentation

    Flatten the two subtypes without changing their subspace topology.

    def smallStarHomeomorph (x : Carrier K) (ε : ℝ) :
    smallStar K x ε ≃ₜ smallStarAmbient K x ε where
…

    Mentions: OAI.HyperbolicObstruction.FinitePolyhedron.Carrier, OAI.HyperbolicObstruction.FinitePolyhedron.smallStar, OAI.HyperbolicObstruction.FinitePolyhedron.smallStarAmbient

  11. lemma OAI.HyperbolicObstruction.FinitePolyhedron.smallStar_contractible line 83
  12. lemma OAI.HyperbolicObstruction.FinitePolyhedron.smallStar_nhds line 89
  13. instance OAI.HyperbolicObstruction.FinitePolyhedron.stronglyLocallyContractible line 95