OAI/GroupTheory/FiniteType/SequentialColimitRangeInclMono.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SequentialColimit.range_incl_mono line 13
  2. lemma OAI.SequentialColimit.finite_subset_stage line 17
  3. lemma OAI.SequentialColimit.isClosed_iff_stages line 30
  4. lemma OAI.SequentialColimit.compact_subset_stage line 38
  5. lemma OAI.SequentialColimit.compact_map_factors line 78
  6. lemma OAI.SequentialCoreTower.compact_map_factors_above line 108
  7. abbrev OAI.SequentialCW.Cell line 134
  8. abbrev OAI.SequentialCW.Space line 140
  9. abbrev OAI.SequentialCW.FinalCell line 141
  10. def OAI.SequentialCW.cellMk line 142
  11. def OAI.SequentialCW.repr line 143
  12. lemma OAI.SequentialCW.repr_eq line 145
  13. def OAI.SequentialCW.stageChart line 154
  14. lemma OAI.SequentialCW.stageChart_apply line 159
  15. lemma OAI.SequentialCW.stageChart_source line 161
  16. lemma OAI.SequentialCW.stageChart_continuousOn line 164
  17. lemma OAI.SequentialCW.stageChart_continuousOn_symm line 167
  18. lemma OAI.SequentialCW.stageChart_eq line 175
  19. def OAI.SequentialCW.chart line 183
  20. lemma OAI.SequentialCW.chart_mk line 187
  21. lemma OAI.SequentialCW.chart_source line 191
  22. lemma OAI.SequentialCW.chart_continuousOn line 193
  23. lemma OAI.SequentialCW.chart_continuousOn_symm line 195
  24. lemma OAI.SequentialCW.chart_union line 200
  25. lemma OAI.SequentialCW.cellMk_map line 211
  26. lemma OAI.SequentialCW.chart_cell_eq line 222
  27. lemma OAI.SequentialCW.chart_pairwiseDisjoint line 252
  28. lemma OAI.SequentialCW.chart_mapsTo line 261
  29. lemma OAI.SequentialCW.chart_image line 282
  30. lemma OAI.SequentialCW.chart_closed line 289
  31. def OAI.SequentialCW.cwComplex line 303
  32. lemma OAI.SequentialCW.cellMk_surjective line 314
  33. lemma OAI.SequentialCW.finiteType line 324