OAI/Geometry/HyperbolicGroups/PictureContact.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PictureSwitch.PictureMap.SelectedSide line 17
2. abbrev OAI.HyperbolicObstruction.PictureSwitch.PictureMap.InternalSide line 18
3. abbrev OAI.HyperbolicObstruction.PictureSwitch.PictureMap.BoundarySide line 19
4. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.number line 20
5. abbrev OAI.HyperbolicObstruction.PictureSwitch.PictureMap.Contact line 21
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.number_ne line 24
7. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.contactSide line 28
8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.contactSide_injective line 33
9. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.contactSide_surjective line 48
10. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.internal_card line 60
11. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryInternalSide line 66
12. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundaryInternalSide_bijective line 72
13. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundary_contacts_eq line 89

    Source documentation

    Exact side counting for an arbitrary selection of faces: each kept internal pairing uses two selected sides, each boundary side one.

    theorem boundary_contacts_eq : Fintype.card (P.BoundarySide selected raw) +
        2 * Fintype.card (P.Contact selected raw) = Fintype.card (SelectedSide selected raw) := by
    …

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.SelectedSide