OAI/Geometry/HyperbolicGroups/PictureVertexBoundary.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PictureSwitch.PictureMap.VertexTransition line 23
2. def OAI.HyperbolicObstruction.PictureSwitch.PictureMap.transitionSide line 25
3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.edge_previous_face line 28
4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.transition_previous_selected line 32
5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.transitionSide_properties line 36
6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.transitionSide_recover line 60
7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.transitionSide_injective line 69
8. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.vertex_transitions_le_boundary line 81

   Source documentation

   Every change of selection at an apex link charges a distinct actual radial boundary side. The two orientations are handled by the unique apex end.

   theorem vertex_transitions_le_boundary : Fintype.card (P.VertexTransition apex selected) ≤
       Fintype.card (P.BoundarySide (fun x => selected x = true) radial) := by
   …