OAI/GroupTheory/FiniteType/CoveringCellGeometry.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CoveringCellGeometry.characteristicLift_isClosedMap line 14
  2. theorem OAI.CoveringCellGeometry.finite_sheets_meeting line 22
  3. theorem OAI.CoveringCellGeometry.isClosed_discrete_slices line 55
  4. abbrev OAI.CoveringCW.Disk line 74
  5. instance OAI.CoveringCW.disk_contractible line 75
  6. abbrev OAI.CoveringCW.BaseCell line 78
  7. def OAI.CoveringCW.baseChar line 80
  8. abbrev OAI.CoveringCW.Fiber line 83
  9. abbrev OAI.CoveringCW.Cell line 86
  10. def OAI.CoveringCW.characteristic line 88
  11. theorem OAI.CoveringCW.characteristic_on_disk line 92
  12. theorem OAI.CoveringCW.characteristic_proj line 96
  13. theorem OAI.CoveringCW.characteristic_continuousOn line 103
  14. theorem OAI.CoveringCW.characteristic_injOn line 114
  15. def OAI.CoveringCW.chart line 123
  16. theorem OAI.CoveringCW.chart_coe line 126
  17. theorem OAI.CoveringCW.chart_source line 128
  18. theorem OAI.CoveringCW.chart_target line 130
  19. theorem OAI.CoveringCW.chart_proj line 133
  20. theorem OAI.CoveringCW.chart_continuousOn line 137
  21. theorem OAI.CoveringCW.chart_symm_eq line 140
  22. theorem OAI.CoveringCW.chart_continuousOn_symm line 148
  23. theorem OAI.CoveringCW.chart_cell_eq line 156
  24. theorem OAI.CoveringCW.chart_pairwiseDisjoint line 180
  25. theorem OAI.CoveringCW.chart_union line 188
  26. theorem OAI.CoveringCW.chart_closedCell_eq_range line 210
  27. theorem OAI.CoveringCW.chart_isCompact line 220
  28. def OAI.CoveringCW.meetingCells line 228
  29. theorem OAI.CoveringCW.mem_meetingCells line 234
  30. theorem OAI.CoveringCW.chart_mapsTo line 241
  31. theorem OAI.CoveringCW.closed_over_cell line 272
  32. theorem OAI.CoveringCW.base_isOpen_of_cells line 303
  33. theorem OAI.CoveringCW.chart_closed_general line 322
  34. def OAI.CoveringCW.meetingCellsOver line 360
  35. theorem OAI.CoveringCW.chart_mapsTo_general line 365
  36. def OAI.CoveringCW.cwComplex_general line 394