OAI/Geometry/HyperbolicGroups/WalkMultiplicity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RawPositionSide line 26
2. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 28) line 28
3. abbrev OAI.HyperbolicObstruction.ConeSkeleton.KindFace line 31
4. instance OAI.HyperbolicObstruction.ConeSkeleton.(instance at line 32) line 32
5. lemma OAI.HyperbolicObstruction.ConeSkeleton.raw_kind line 35
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.raw_multiplicity_le_faces line 43

   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 (walkFrozenTarget n w d c hc f)) (p : RawPosition n w d) :
       Fintype.card (RawPositionSide n w d c hc f P select p) ≤
         Fintype.card (KindFace n w d c hc f P select (walkKind n w d (rawRepresentative n w d p))) := by
   …

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

7. lemma OAI.HyperbolicObstruction.ConeSkeleton.raw_fan_index line 59
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.raw_fan_previous line 76
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.raw_fan_previous_start line 83
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.raw_fan_multiplicity_le line 91

    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 (walkFrozenTarget n w d c hc f))
        (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w)) (g : FanTriangle n w) :
        Fintype.card (RawPositionSide n w d c hc f P select (.inr (.inl g))) ≤
          Fintype.card (ApexInstance n w d c hc f P select g.1) := by
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.walkFrozenTarget, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle, OAI.HyperbolicObstruction.ConeSkeleton.RawPositionSide, OAI.HyperbolicObstruction.ConeSkeleton.ApexInstance