OAI/GroupTheory/FiniteType/CWCylinder.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CWCylinder.Disk line 14
  2. abbrev OAI.CWCylinder.Boundary line 15
  3. theorem OAI.CWCylinder.norm_cons line 17
  4. theorem OAI.CWCylinder.norm_tail_le line 31
  5. theorem OAI.CWCylinder.norm_eq_max line 36
  6. theorem OAI.CWCylinder.time_bound line 41
  7. def OAI.CWCylinder.encode line 45
  8. def OAI.CWCylinder.diskTail line 51
  9. def OAI.CWCylinder.diskTime line 61
  10. theorem OAI.CWCylinder.encode_tail line 71
  11. theorem OAI.CWCylinder.encode_time line 76
  12. theorem OAI.CWCylinder.encode_decode line 81
  13. theorem OAI.CWCylinder.encode_injective line 88
  14. def OAI.CWCylinder.bottom line 92
  15. def OAI.CWCylinder.top line 99
  16. def OAI.CWCylinder.side line 106
  17. abbrev OAI.CWCylinder.Faces line 113
  18. def OAI.CWCylinder.faceQuot line 115
  19. theorem OAI.CWCylinder.faceQuot_surjective line 120
  20. theorem OAI.CWCylinder.faceQuot_isQuotientMap line 149
  21. def OAI.CWCylinder.boundaryDisk line 152
  22. def OAI.CWCylinder.faceCylinder line 155
  23. theorem OAI.CWCylinder.face_encode line 158
  24. theorem OAI.CWCylinder.faceCylinder_eq_of_faceQuot_eq line 169
  25. def OAI.CWCylinder.faceData line 174
  26. theorem OAI.CWCylinder.faceData_factors line 178
  27. def OAI.CWCylinder.boundaryMap line 216
  28. theorem OAI.CWCylinder.boundaryMap_face line 221
  29. def OAI.CWCylinder.SphereFill line 227
  30. theorem OAI.CWCylinder.exists_cylinder line 230