OAI/GroupTheory/FiniteType/PresentationVanKampen.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PresentationVanKampen.intervalPath line 11
  2. theorem OAI.PresentationVanKampen.intervalPath_self line 19
  3. theorem OAI.PresentationVanKampen.intervalPath_zero_one line 24
  4. theorem OAI.PresentationVanKampen.intervalPath_mem line 28
  5. def OAI.PresentationVanKampen.portion line 40
  6. theorem OAI.PresentationVanKampen.portion_self line 43
  7. theorem OAI.PresentationVanKampen.portion_trans line 48
  8. theorem OAI.PresentationVanKampen.portion_mem line 55
  9. theorem OAI.PresentationVanKampen.path_induction_open_cover line 61
  10. def OAI.PresentationVanKampen.basedPathClass line 96
  11. theorem OAI.PresentationVanKampen.basedPathClass_refl line 101
  12. theorem OAI.PresentationVanKampen.basedPathClass_trans line 107
  13. theorem OAI.PresentationVanKampen.basedPathClass_homotopic line 115
  14. theorem OAI.PresentationVanKampen.basedPathClass_loop line 121
  15. theorem OAI.PresentationVanKampen.subgroup_eq_top_of_open_cover line 130
  16. def OAI.PresentationVanKampen.pathIn line 149
  17. theorem OAI.PresentationVanKampen.pathIn_map line 156
  18. theorem OAI.PresentationVanKampen.homotopic_in_simplyConnected line 160
  19. def OAI.PresentationVanKampen.Replaceable line 167
  20. theorem OAI.PresentationVanKampen.replaceable_refl line 172
  21. theorem OAI.PresentationVanKampen.replaceable_trans line 178
  22. theorem OAI.PresentationVanKampen.replaceable_homotopic line 192
  23. theorem OAI.PresentationVanKampen.replaceable_of_range_subset line 198
  24. theorem OAI.PresentationVanKampen.replaceable_of_simplyConnected line 210
  25. theorem OAI.PresentationVanKampen.replaceable_of_open_cover line 225
  26. theorem OAI.PresentationVanKampen.cancel_spoke line 234
  27. theorem OAI.PresentationVanKampen.fundamentalGroupMap_surjective_of_open_cover line 243
  28. theorem OAI.PresentationVanKampen.exists_compatible_spokes line 289
  29. theorem OAI.PresentationVanKampen.fundamentalGroupMap_surjective_of_disjoint_open_cover line 321