OAI/Geometry/HyperbolicGroups/RelativeMultiplicity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.RawPositionSide line 26
2. instance OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.(instance at line 28) line 28
3. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.KindFace line 31
4. instance OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.(instance at line 32) line 32
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.raw_multiplicity_le_faces line 37

   Source documentation

   Top loose fields and every decoration field occur at most once in each selected source face of that occurrence.

   lemma raw_multiplicity_le_faces (hs : P.Simple) (hb : P.NoBigon)
       (hm : P.FrozenMapped (frozen n w d ell hell word c hc f)) (p : RawPosition n w d) :
       Fintype.card (RawPositionSide n w d ell hell word c hc f P select p) ≤
         Fintype.card (KindFace n w d ell hell word c hc f P select (walkKind n w d (rawRepresentative n w d p))) := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.frozen, OAI.HyperbolicObstruction.ConeSkeleton.RawPosition, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.RawPositionSide, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.KindFace, OAI.HyperbolicObstruction.ConeSkeleton.walkKind, OAI.HyperbolicObstruction.ConeSkeleton.rawRepresentative

6. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.raw_fan_index line 56
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.raw_fan_previous line 74
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.raw_fan_previous_start line 81
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.raw_fan_multiplicity_le line 89

   Source documentation

   A fan field's selected copies inject into the ACTUAL represented apex instances, not into an assumed nominal collection of links.

   lemma raw_fan_multiplicity_le (hm : P.FrozenMapped (frozen n w d ell hell word c hc f))
       (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w)) (g : FanTriangle n w) :
       Fintype.card (RawPositionSide n w d ell hell word c hc f P select (.inr (.inl g))) ≤
         Fintype.card (ApexInstance n w d ell hell word c hc f P select g.1) := by
   …

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.frozen, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.RawPositionSide, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.ApexInstance