OAI/GroupTheory/Kervaire/ComponentFibers.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KervaireRibbon.Fiber line 14
  2. def OAI.KervaireRibbon.fiberPerm line 16
  3. lemma OAI.KervaireRibbon.fiberPerm_apply line 23
  4. lemma OAI.KervaireRibbon.numCycles_fiber_sum line 27
  5. lemma OAI.KervaireRibbon.card_fiber_sum line 42
  6. lemma OAI.KervaireRibbon.fiberPerm_mul line 46
  7. lemma OAI.KervaireRibbon.fiber_connected line 52
  8. lemma OAI.KervaireRibbon.classes_top line 92
  9. lemma OAI.KervaireRibbon.planar_fiber line 96
  10. lemma OAI.KervaireRibbon.sameCycle_involution line 139
  11. lemma OAI.KervaireRibbon.card_fiber_involution line 156
  12. lemma OAI.KervaireRibbon.numCycles_involution line 178
  13. lemma OAI.KervaireRibbon.numCycles_eq_card_of_projection line 186
  14. lemma OAI.KervaireRibbon.numCycles_equiv line 195
  15. lemma OAI.KervaireRibbon.reachable_of_cycle line 213
  16. lemma OAI.KervaireRibbon.reachable_of_component line 224