OAI/Geometry/HyperbolicGroups/PolygonBoundaryList.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.positiveSides line 19

    Source documentation

    The literal positive indexed attaching word, with no quotienting of repeated labels or cyclic starting positions.

    def positiveSides (c : C) : List B.Side :=
…
  2. def OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.attachingWord line 22
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.positiveSides_boundary line 24
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.positiveSides_label line 32
  5. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.positiveSides_mem line 36
  6. def OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.withOutside line 45

    Source documentation

    A single additional outside polygon, with a separate cell index.

    def withOutside : PolygonTarget.Boundary (C ⊕ Unit) L V where
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary

  7. def OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.outsideTag line 56

    Source documentation

    none marks every genuine target cell, while the two exterior orientations remain separately identifiable.

    def outsideTag : (B.withOutside ell hell word closed).Side → Option Bool :=
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.Side

  8. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.positive_inside_tag line 59
  9. lemma OAI.HyperbolicObstruction.PictureSwitch.PolygonTarget.Boundary.positive_outside_tag line 66