OAI/Geometry/HyperbolicGroups/RelativeDegree.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.oriented_boundary line 16

   Source documentation

   The two orientations have exactly the same indexed perimeter.

   lemma oriented_boundary (s : B.Side) :
       ∃ ys : List B.Side, IsBoundary B.next ys ∧ s ∈ ys ∧ ys.length = B.size s.1 := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary

2. lemma OAI.HyperbolicObstruction.PictureSwitch.WalkPicture.FrozenMapped.face_card line 44
3. lemma OAI.HyperbolicObstruction.ConeSkeleton.exterior_top_degree line 67
4. lemma OAI.HyperbolicObstruction.ConeSkeleton.exterior_frozen_degree line 96
5. theorem OAI.HyperbolicObstruction.ConeSkeleton.exterior_interior_degree line 120

   Source documentation

   The actual interior dual multigraph of a protected normal disk has the source's uniform bound15. The arbitrary exterior degree is not bounded.

   theorem exterior_interior_degree (hs : P.Simple) (hb : P.NoBigon)
       (hm : P.FrozenMapped (exteriorWalkFrozen n w d ell hell word closed c hc f))
       (x : P.Dart)
       (hx : ¬ (walkTarget n w d c hc f).isExterior ell hell word closed (P.index x)) :
       Fintype.card {y : P.Dart // P.pairing.face.SameCycle x y} ≤ 15 := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.exteriorWalkFrozen, OAI.HyperbolicObstruction.ConeSkeleton.walkTarget