OAI/Geometry/HyperbolicGroups/FaceChainSelection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Counting one selected position on each actual indexed face.

  1. lemma OAI.HyperbolicObstruction.PictureSwitch.faceChain_eq_selected line 19
  2. lemma OAI.HyperbolicObstruction.PictureSwitch.faceChain_eq_ite line 39
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.IndexedFaceMap.selected line 46
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.cell_cycle line 61
  5. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.marked_unique line 65