OAI/GroupTheory/FiniteType/PresentationVanKampenRectanglePaths.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PresentationVanKampen.rectangle_paths line 11
  2. theorem OAI.PresentationGeometry.Cells.collarToShell_disk line 51
  3. def OAI.PresentationGeometry.Rose.outward line 67
  4. theorem OAI.PresentationGeometry.Rose.outward_base line 74
  5. theorem OAI.PresentationGeometry.Rose.collar_path_homotopic line 83
  6. theorem OAI.PresentationGeometry.Rose.radialDisk_one_cases line 112
  7. theorem OAI.PresentationGeometry.Rose.spoke_outward_mem line 136
  8. theorem OAI.PresentationGeometry.Rose.basedPathClass_collar_mem line 214
  9. theorem OAI.PresentationGeometry.Rose.freeToFundamental_surjective line 236
  10. theorem OAI.PresentationGeometry.PresentationComplex.freeToFundamental_surjective line 273
  11. theorem OAI.PresentationGeometry.PresentationComplex.presentedToFundamental_surjective line 277
  12. def OAI.PresentationGeometry.Rose.coverSet line 291
  13. theorem OAI.PresentationGeometry.Rose.coverSet_isOpen line 295
  14. theorem OAI.PresentationGeometry.Rose.mem_coverSet line 300
  15. theorem OAI.PresentationGeometry.Rose.overlap_coord_ne_zero line 308
  16. def OAI.PresentationGeometry.Rose.potential line 327
  17. theorem OAI.PresentationGeometry.Rose.potential_none line 335
  18. theorem OAI.PresentationGeometry.Rose.potential_continuous_overlap line 339
  19. def OAI.PresentationGeometry.Rose.transition line 363
  20. theorem OAI.PresentationGeometry.Rose.continuousOn_transition line 366
  21. def OAI.PresentationGeometry.Rose.coveringCore line 407
  22. theorem OAI.PresentationGeometry.Rose.coveringCore_isCoveringMap line 417
  23. theorem OAI.PresentationGeometry.Rose.edgeMap_mem_interior line 426
  24. theorem OAI.PresentationGeometry.Rose.openEdgeLift_edgeMap line 431
  25. def OAI.PresentationGeometry.Rose.edgeNegative line 441
  26. def OAI.PresentationGeometry.Rose.edgePositive line 442
  27. theorem OAI.PresentationGeometry.Rose.norm_edgeNegative line 444
  28. theorem OAI.PresentationGeometry.Rose.norm_edgePositive line 446
  29. def OAI.PresentationGeometry.Rose.edgeFirst line 449
  30. def OAI.PresentationGeometry.Rose.edgeMiddle line 452
  31. def OAI.PresentationGeometry.Rose.edgeLast line 455
  32. theorem OAI.PresentationGeometry.Rose.edgeFirst_collar line 458
  33. theorem OAI.PresentationGeometry.Rose.edgeMiddle_interior line 474
  34. theorem OAI.PresentationGeometry.Rose.edgeLast_collar line 484
  35. theorem OAI.PresentationGeometry.Rose.edge_parts_homotopic line 500
  36. theorem OAI.PresentationGeometry.Rose.potential_negative line 519
  37. theorem OAI.PresentationGeometry.Rose.potential_positive line 526
  38. theorem OAI.PresentationGeometry.Rose.monodromy_generator line 532