OAI/GroupTheory/FiniteType/DiskRadial.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.DiskRadial.Disk line 14
  2. def OAI.DiskRadial.denom line 16
  3. lemma OAI.DiskRadial.denom_pos line 17
  4. lemma OAI.DiskRadial.le_denom line 18
  5. lemma OAI.DiskRadial.continuous_denom line 19
  6. def OAI.DiskRadial.inflate line 23
  7. lemma OAI.DiskRadial.continuous_inflate line 28
  8. lemma OAI.DiskRadial.norm_inflate line 33
  9. lemma OAI.DiskRadial.norm_le_inflate line 36
  10. lemma OAI.DiskRadial.inflate_boundary line 42
  11. lemma OAI.DiskRadial.norm_inflate_of_half_lt line 46
  12. def OAI.DiskRadial.radial line 49
  13. lemma OAI.DiskRadial.continuous_radial line 53
  14. lemma OAI.DiskRadial.radial_zero line 60
  15. lemma OAI.DiskRadial.radial_one line 61
  16. lemma OAI.DiskRadial.radial_boundary line 62
  17. lemma OAI.DiskRadial.norm_radial line 68
  18. lemma OAI.DiskRadial.norm_le_radial line 75
  19. def OAI.CWCollar.radius line 88
  20. lemma OAI.CWCollar.radius_prior line 92
  21. lemma OAI.CWCollar.radius_disk line 94
  22. def OAI.CWCollar.lower line 97
  23. theorem OAI.CWCollar.radius_eq_one_iff line 99
  24. def OAI.CWCollar.collar line 112
  25. lemma OAI.CWCollar.collar_open line 113
  26. lemma OAI.CWCollar.lower_subset_collar line 114
  27. def OAI.CWCollar.paths line 120
  28. lemma OAI.CWCollar.paths_prior line 133
  29. lemma OAI.CWCollar.paths_disk line 137
  30. lemma OAI.CWCollar.paths_zero line 143
  31. lemma OAI.CWCollar.paths_fixed line 150
  32. lemma OAI.CWCollar.radius_le_paths line 153
  33. lemma OAI.CWCollar.paths_mem_collar line 162
  34. lemma OAI.CWCollar.paths_one_lower line 165
  35. lemma OAI.CWCollar.lower_closed line 184
  36. def OAI.CWCollar.collarInclusion line 191
  37. def OAI.CWCollar.retract line 194
  38. def OAI.CWCollar.collarHomotopy line 198
  39. def OAI.CWCollar.collarEquiv line 205
  40. abbrev OAI.CWCollar.OpenDisk line 216
  41. abbrev OAI.CWCollar.OpenCells line 217
  42. def OAI.CWCollar.openDom line 219
  43. lemma OAI.CWCollar.openDom_embedding line 222
  44. lemma OAI.CWCollar.openDom_mem line 226
  45. def OAI.CWCollar.openPreimage line 233
  46. lemma OAI.CWCollar.openPreimage_surjective line 236
  47. def OAI.CWCollar.openPreimageEquiv line 246
  48. def OAI.CWCollar.openCellMap line 249
  49. lemma OAI.CWCollar.openCellMap_quotient line 252
  50. lemma OAI.CWCollar.openCellMap_injective line 255
  51. def OAI.CWCollar.openCellsEquiv line 269
  52. lemma OAI.CWCollar.openCellsEquiv_apply line 272