OAI/Geometry/HyperbolicGroups/FiniteFanData.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.FanLink.Mark.map line 15
2. lemma OAI.HyperbolicObstruction.FanLink.Mark.map_absent line 19
3. lemma OAI.HyperbolicObstruction.FanLink.Mark.map_triangle line 20
4. lemma OAI.HyperbolicObstruction.FanLink.Mark.map_top line 21
5. structure OAI.HyperbolicObstruction.FanLink.IndexedFanData line 27

   Source documentation

   The same local finite-link data, with natural geometric index types. toFin is only a change of finite coordinates, not an additional assumption.

   structure IndexedFanData (I F O : Type*) (L : I → Type*) [Fintype I] [Fintype F] [Fintype O]
       [∀ z, Fintype (L z)] where
   …

6. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.numberLink line 46
7. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.linkEquiv line 48
8. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.nextFin line 51
9. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.nextFin_symm line 54
10. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.nextFin_cyclic line 59
11. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.markFin line 69
12. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.decode line 72
13. lemma OAI.HyperbolicObstruction.FanLink.IndexedFanData.decode_injective line 75
14. def OAI.HyperbolicObstruction.FanLink.IndexedFanData.toFin line 87

    Source documentation

    Transport to the already proved finite-coordinate fan inequality.

    def toFin : FanData (Fintype.card I) (Fintype.card F) (Fintype.card O) where
    …

    Mentions: OAI.HyperbolicObstruction.FanLink.FanData