OAI/Geometry/IsometricImmersion/Assembly/AccumulatingDisks.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SmoothLocal.Geometry.accumulatingScale line 13
  2. def OAI.SmoothLocal.Geometry.accumulatingCenter line 15
  3. def OAI.SmoothLocal.Geometry.accumulatingRadius line 17
  4. def OAI.SmoothLocal.Geometry.accumulatingDisk line 19
  5. def OAI.SmoothLocal.Geometry.enlargedAccumulatingDisk line 22
  6. theorem OAI.SmoothLocal.Geometry.accumulatingScale_pos line 25
  7. theorem OAI.SmoothLocal.Geometry.accumulatingScale_le_half line 28
  8. theorem OAI.SmoothLocal.Geometry.accumulatingScale_succ line 31
  9. theorem OAI.SmoothLocal.Geometry.accumulatingScale_antitone line 36
  10. theorem OAI.SmoothLocal.Geometry.accumulatingScale_le_half_of_lt line 40
  11. theorem OAI.SmoothLocal.Geometry.accumulatingRadius_pos line 45
  12. theorem OAI.SmoothLocal.Geometry.roundClosedDisk_coord_abs_le line 48
  13. theorem OAI.SmoothLocal.Geometry.accumulatingDisk_subset_enlarged line 58
  14. theorem OAI.SmoothLocal.Geometry.accumulatingDisk_subset_enlarged_open line 65
  15. theorem OAI.SmoothLocal.Geometry.enlargedAccumulatingDisk_bounds line 72
  16. theorem OAI.SmoothLocal.Geometry.enlargedAccumulatingDisk_disjoint_of_lt line 86
  17. theorem OAI.SmoothLocal.Geometry.enlargedAccumulatingDisks_pairwise_disjoint line 96
  18. theorem OAI.SmoothLocal.Geometry.accumulatingDisks_pairwise_disjoint line 103
  19. theorem OAI.SmoothLocal.Geometry.enlargedAccumulatingDisk_subset_square line 109
  20. theorem OAI.SmoothLocal.Geometry.accumulatingDisk_subset_square line 121
  21. theorem OAI.SmoothLocal.Geometry.zero_not_mem_enlargedAccumulatingDisk line 124
  22. theorem OAI.SmoothLocal.Geometry.zero_not_mem_accumulatingDisk line 132
  23. theorem OAI.SmoothLocal.Geometry.accumulatingDisk_isCompact line 135
  24. theorem OAI.SmoothLocal.Geometry.enlargedAccumulatingDisk_isCompact line 138
  25. theorem OAI.SmoothLocal.Geometry.accumulatingDisk_interior_nonempty line 141
  26. theorem OAI.SmoothLocal.Geometry.tendsto_accumulatingScale line 144
  27. theorem OAI.SmoothLocal.Geometry.tendsto_accumulatingCenter line 150
  28. theorem OAI.SmoothLocal.Geometry.enlargedAccumulatingDisk_norm_le line 159
  29. theorem OAI.SmoothLocal.Geometry.eventually_enlargedAccumulatingDisk_subset line 172
  30. theorem OAI.SmoothLocal.Geometry.eventually_accumulatingDisk_subset line 184
  31. theorem OAI.SmoothLocal.Geometry.eventually_all_accumulatingDisks_in_open line 189
  32. theorem OAI.SmoothLocal.Geometry.enlargedAccumulatingDisks_locallyFinite_away_zero line 194
  33. theorem OAI.SmoothLocal.Geometry.enlargedAccumulatingDisks_locallyFinite_punctured line 208
  34. theorem OAI.SmoothLocal.Geometry.accumulatingDisks_locallyFinite_punctured line 219