OAI/Geometry/HyperbolicGroups/BoundarySplice.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicObstruction.PictureSwitch.formPerm_append_join line 16
2. theorem OAI.HyperbolicObstruction.PictureSwitch.IsBoundary.splice_append line 32

   Source documentation

   Concatenation is the literal connected-sum splice at the two incoming corners. The side order, not merely the freely represented word, is retained.

   theorem splice_append (hl : IsBoundary f (l++[a])) (hr : IsBoundary f (b::r))
       (hd : ∀ x ∈ l++[a], x ∉ b::r) :
       IsBoundary (f * swap a ((b::r).getLast (by simp))) ((l++[a])++(b::r)) := by
   …

   Mentions: OAI.HyperbolicObstruction.PictureSwitch.IsBoundary