OAI/GroupTheory/FiniteType/DiskHEP.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DiskHEP.Disk line 11
  2. abbrev OAI.DiskHEP.Boundary line 12
  3. abbrev OAI.DiskHEP.Corner line 13
  4. def OAI.DiskHEP.den line 15
  5. def OAI.DiskHEP.ratio line 16
  6. lemma OAI.DiskHEP.norm_le line 18
  7. lemma OAI.DiskHEP.den_pos line 21
  8. lemma OAI.DiskHEP.den_le line 24
  9. lemma OAI.DiskHEP.ratio_pos line 27
  10. lemma OAI.DiskHEP.ratio_ge line 28
  11. lemma OAI.DiskHEP.ratio_mul_den line 31
  12. lemma OAI.DiskHEP.time_bounds line 34
  13. lemma OAI.DiskHEP.point_bound line 44
  14. lemma OAI.DiskHEP.hits_corner line 51
  15. lemma OAI.DiskHEP.continuous_ratio line 66
  16. def OAI.DiskHEP.retract line 73
  17. lemma OAI.DiskHEP.ratio_eq_one line 81
  18. lemma OAI.DiskHEP.retract_corner line 93
  19. def OAI.DiskHEP.boundaryInclusion line 104
  20. def OAI.DiskHEP.bottom line 107
  21. def OAI.DiskHEP.side line 110
  22. def OAI.DiskHEP.cornerQuot line 115
  23. theorem OAI.DiskHEP.cornerQuot_surjective line 118
  24. theorem OAI.DiskHEP.cornerQuot_isQuotientMap line 126
  25. def OAI.DiskHEP.cornerData line 132
  26. theorem OAI.DiskHEP.cornerData_factors line 136
  27. def OAI.DiskHEP.extend line 165
  28. lemma OAI.DiskHEP.extend_corner line 169
  29. theorem OAI.DiskHEP.extend_zero line 177
  30. theorem OAI.DiskHEP.extend_side line 182
  31. abbrev OAI.SimplexBoundary.Simplex line 192
  32. abbrev OAI.SimplexBoundary.Boundary line 193
  33. def OAI.SimplexBoundary.face line 195
  34. lemma OAI.SimplexBoundary.face_zero line 198
  35. lemma OAI.SimplexBoundary.face_succAbove line 201
  36. def OAI.SimplexBoundary.drop line 205
  37. lemma OAI.SimplexBoundary.face_drop line 215
  38. def OAI.SimplexBoundary.faceQuot line 226
  39. theorem OAI.SimplexBoundary.faceQuot_surjective line 230
  40. theorem OAI.SimplexBoundary.faceQuot_isQuotientMap line 235
  41. def OAI.SimplexBoundary.boundaryEquiv line 238
  42. def OAI.SimplexBoundary.glueFaces line 261
  43. theorem OAI.SimplexBoundary.glueFaces_face line 267