OAI/GroupTheory/Kervaire/Splicing.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.KervaireRibbon.splice line 13
  2. lemma OAI.KervaireRibbon.splice_inl line 16
  3. lemma OAI.KervaireRibbon.splice_inr line 28
  4. lemma OAI.KervaireRibbon.splice_marker line 36
  5. lemma OAI.KervaireRibbon.chain_redirect line 40
  6. lemma OAI.KervaireRibbon.circle_splice line 57
  7. lemma OAI.KervaireRibbon.planar_splice line 82
  8. lemma OAI.KervaireRibbon.planar_vertex_join_face line 108
  9. lemma OAI.KervaireRibbon.planar_one_left line 124
  10. def OAI.KervaireRibbon.whisker line 129
  11. lemma OAI.KervaireRibbon.whisker_o line 134
  12. lemma OAI.KervaireRibbon.whisker_y line 137
  13. lemma OAI.KervaireRibbon.whisker_x line 140
  14. lemma OAI.KervaireRibbon.whisker_inl line 147
  15. lemma OAI.KervaireRibbon.planar_whisker line 155
  16. lemma OAI.KervaireRibbon.circle_whisker line 174