OAI/Geometry/HyperbolicGroups/BoundaryEnumeration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HyperbolicObstruction.PictureSwitch.exists_boundary line 18

   Source documentation

   Every finite face orbit has a literal nonempty boundary enumeration, including monogons (which Perm.toList alone omits).

   theorem exists_boundary (p : Perm D) (a : D) :
       ∃ xs, IsBoundary p xs ∧ a ∈ xs := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary

2. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.length_eq_card line 32