OAI/Geometry/HyperbolicGroups/MergeWalk.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_respects line 21
  2. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_kind line 35
  3. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_face_of_away line 43
  4. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_face_hit_left line 51
  5. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_face_hit_right line 59
  6. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_closed_local line 70

    Source documentation

    Closure in indexed template vertices is retained even though adjacent polygons belonging to OTHER occurrences use different template vertex types. Only the two cancelling sides need agree as opposite template steps.

    lemma mergeEdge_closed_local {source target : D → V} (hc : M.FaceClosed source target)
    (ha : source a = target b) (hb : source b = target a) :
    (M.mergeEdge h).FaceClosed (source ∘ Subtype.val) (target ∘ Subtype.val) := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.FaceClosed

  7. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_face_frozen line 86

    Source documentation

    Any frozen kind disjoint from the cancelled kind retains its complete face cycles and side indices under the common-side cancellation.

    lemma mergeEdge_face_frozen {kind : D → C} (hk : M.FaceKind kind)
    (free : C → Bool) (ha : free (kind a) = true) (hb : free (kind b) = true)
    (x : {x // OffPair a b x}) (hx : free (kind x.val) = false) :
    ((M.mergeEdge h).face x).val = M.face x.val := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.OffPair

  8. lemma OAI.HyperbolicObstruction.PictureSwitch.PictureMap.mergeEdge_closed line 103

    Source documentation

    Closed target face walks remain closed after deleting the common side. This uses only edge reversal and original closure, and is unaffected by any other common vertices or edges of the two polygons.

    lemma mergeEdge_closed {source target : D → V} (hc : M.FaceClosed source target)
    (he : ∀ x, source (M.edge x) = target x) :
    (M.mergeEdge h).FaceClosed (source ∘ Subtype.val) (target ∘ Subtype.val) := by
…

    Mentions: OAI.HyperbolicObstruction.PictureSwitch.PictureMap.FaceClosed