OAI/GroupTheory/FiniteType/SequentialColimit.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SequentialColimit.Space line 14
  2. def OAI.SequentialColimit.incl line 16
  3. lemma OAI.SequentialColimit.incl_map line 19
  4. lemma OAI.SequentialColimit.incl_injective line 22
  5. def OAI.SequentialColimit.lift line 25
  6. lemma OAI.SequentialColimit.lift_incl line 31
  7. def OAI.SequentialColimit.extendOne line 37
  8. lemma OAI.SequentialColimit.extendOne_eq line 41
  9. def OAI.SequentialColimit.extendTail line 49
  10. lemma OAI.SequentialColimit.extendTail_compat line 53
  11. def OAI.SequentialColimit.extendFamily line 63
  12. lemma OAI.SequentialColimit.extendFamily_compat line 66
  13. def OAI.SequentialColimit.extend line 73
  14. lemma OAI.SequentialColimit.extend_eq line 76
  15. theorem OAI.SequentialColimit.hausdorff line 85
  16. lemma OAI.SequentialColimit.incl_isClosedEmbedding line 98
  17. lemma OAI.SequentialColimit.isOpen_iff_stages line 110
  18. lemma OAI.SequentialColimit.continuousOn_of_stages line 115
  19. def OAI.SequentialCore.baseSet line 136
  20. def OAI.SequentialCore.potential line 140
  21. lemma OAI.SequentialCore.mem_baseSet_incl line 143
  22. lemma OAI.SequentialCore.potential_incl line 146
  23. lemma OAI.SequentialCore.baseSet_open line 155
  24. lemma OAI.SequentialCore.baseSet_cover line 160
  25. lemma OAI.SequentialCore.continuousOn_transition line 170
  26. def OAI.SequentialCore.core line 181
  27. lemma OAI.SequentialCore.core_covering line 191
  28. lemma OAI.SequentialCore.core_surjective line 194
  29. abbrev OAI.SequentialCoreTower.Index line 216
  30. def OAI.SequentialCoreTower.stageSet line 218
  31. def OAI.SequentialCoreTower.stagePot line 222
  32. lemma OAI.SequentialCoreTower.stageSet_common line 226
  33. lemma OAI.SequentialCoreTower.stagePot_common line 240
  34. lemma OAI.SequentialCoreTower.stageSet_compat line 254
  35. lemma OAI.SequentialCoreTower.stagePot_compat line 262
  36. lemma OAI.SequentialCoreTower.stageSet_open line 268
  37. lemma OAI.SequentialCoreTower.stageSet_cover line 278
  38. lemma OAI.SequentialCoreTower.transition_cont line 284
  39. def OAI.SequentialCoreTower.core line 304
  40. lemma OAI.SequentialCoreTower.core_covering line 310
  41. lemma OAI.SequentialCoreTower.baseSet_incl line 329
  42. lemma OAI.SequentialCoreTower.coordChange_incl line 336
  43. def OAI.SequentialCoreTower.coverIncl line 344
  44. lemma OAI.SequentialCoreTower.coverIncl_proj line 351
  45. lemma OAI.SequentialCoreTower.coverIncl_range line 355
  46. lemma OAI.SequentialCoreTower.coverIncl_isClosedEmbedding line 374