OAI/Geometry/HyperbolicGroups/PicturePartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.PictureSwitch.CutSide line 20

   Source documentation

   Oriented side copies cut by a partition. Parallel contacts and self-contacts remain literal side copies; no underlying-simple-graph collapse is made.

   abbrev CutSide (P : PictureMap X) (part : X → I) := {x : X // part x ≠ part (P.edge x)}

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap

2. instance OAI.HyperbolicObstruction.PictureSwitch.(instance at line 21) line 21
3. abbrev OAI.HyperbolicObstruction.PictureSwitch.CutContact line 22
4. instance OAI.HyperbolicObstruction.PictureSwitch.(instance at line 24) line 24
5. abbrev OAI.HyperbolicObstruction.PictureSwitch.PartBoundary line 26
6. instance OAI.HyperbolicObstruction.PictureSwitch.(instance at line 28) line 28
7. lemma OAI.HyperbolicObstruction.PictureSwitch.sum_part_boundary line 30
8. lemma OAI.HyperbolicObstruction.PictureSwitch.cut_sides_twice line 41
9. lemma OAI.HyperbolicObstruction.PictureSwitch.sum_part_sizes line 58