OAI/GroupTheory/UniversalGroup/GraphBundles.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalFInfinity.GraphBundle.Inner line 27
  2. abbrev OAI.UniversalFInfinity.GraphBundle.Core line 28
  3. def OAI.UniversalFInfinity.GraphBundle.Space line 29
  4. def OAI.UniversalFInfinity.GraphBundle.vertex line 30
  5. def OAI.UniversalFInfinity.GraphBundle.interior line 31
  6. def OAI.UniversalFInfinity.GraphBundle.edge line 33
  7. lemma OAI.UniversalFInfinity.GraphBundle.edge_zero line 40
  8. lemma OAI.UniversalFInfinity.GraphBundle.edge_one line 41
  9. lemma OAI.UniversalFInfinity.GraphBundle.edge_inner line 42
  10. abbrev OAI.UniversalFInfinity.GraphBundle.Raw line 52
  11. def OAI.UniversalFInfinity.GraphBundle.quotient line 53
  12. instance OAI.UniversalFInfinity.GraphBundle.(instance at line 55) line 55
  13. lemma OAI.UniversalFInfinity.GraphBundle.continuous_quotient line 59
  14. lemma OAI.UniversalFInfinity.GraphBundle.continuous_vertex line 61
  15. lemma OAI.UniversalFInfinity.GraphBundle.continuous_edge line 64
  16. def OAI.UniversalFInfinity.GraphBundle.vertexMap line 67
  17. def OAI.UniversalFInfinity.GraphBundle.edgeMap line 69
  18. lemma OAI.UniversalFInfinity.GraphBundle.continuous_iff line 72
  19. lemma OAI.UniversalFInfinity.GraphBundle.closed_of_slices line 79
  20. lemma OAI.UniversalFInfinity.GraphBundle.isClosed_iff line 90
  21. def OAI.UniversalFInfinity.GraphBundle.liftFun line 107
  22. lemma OAI.UniversalFInfinity.GraphBundle.liftFun_vertex line 110
  23. lemma OAI.UniversalFInfinity.GraphBundle.liftFun_edge line 113
  24. def OAI.UniversalFInfinity.GraphBundle.lift line 121
  25. lemma OAI.UniversalFInfinity.GraphBundle.lift_vertex line 127
  26. lemma OAI.UniversalFInfinity.GraphBundle.lift_edge line 128
  27. lemma OAI.UniversalFInfinity.GraphBundle.edge_preimage_vertices line 141
  28. lemma OAI.UniversalFInfinity.GraphBundle.base_closedEmbedding line 178
  29. lemma OAI.UniversalFInfinity.GraphBundle.interior_preimage line 201
  30. lemma OAI.UniversalFInfinity.GraphBundle.selection_closed line 253
  31. theorem OAI.UniversalFInfinity.GraphBundle.compact_finitely_many_edges line 292
  32. theorem OAI.UniversalFInfinity.GraphBundle.compact_finitely_many_vertices line 319
  33. lemma OAI.UniversalFInfinity.GraphBundle.vertex_eq_vertex line 339
  34. lemma OAI.UniversalFInfinity.GraphBundle.vertex_ne_interior line 343
  35. lemma OAI.UniversalFInfinity.GraphBundle.interior_ne_vertex line 348
  36. lemma OAI.UniversalFInfinity.GraphBundle.interior_eq_interior line 351
  37. lemma OAI.UniversalFInfinity.GraphBundle.edge_eq_vertex line 356
  38. lemma OAI.UniversalFInfinity.GraphBundle.edgeImage_vertex_slice line 373
  39. lemma OAI.UniversalFInfinity.GraphBundle.edgeImage_vertex_closed line 396