OAI/Geometry/HyperbolicGroups/EdgeEraseBoundary.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.erase_head line 18
2. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.erase_at line 27
3. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.splice_heads line 34

   Source documentation

   The two actual face cycles are spliced at the deleted paired sides.

   lemma splice_heads {f : Perm D} {a b : D} {l r : List D}
       (hl : IsBoundary f (a::l)) (hr : IsBoundary f (b::r))
       (hd : ∀ x ∈ a::l, x ∉ b::r) :
       IsBoundary (f * swap a b) (a::(r++b::l)) := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary

4. lemma OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.splice_heads_offpair line 54
5. theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.eraseEdge_boundary line 74