OAI/Geometry/IsometricImmersion/Caps/NestedCapRectangles.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SmoothLocal.Flow.LowerCapRectangle line 13
  2. def OAI.SmoothLocal.Flow.LowerCapRectangle.region line 30
  3. def OAI.SmoothLocal.Flow.LowerCapRectangle.image line 32
  4. theorem OAI.SmoothLocal.Flow.LowerCapRectangle.region_subset_domain line 34
  5. def OAI.SmoothLocal.Flow.LowerCapRectangle.energyOuter line 37
  6. theorem OAI.SmoothLocal.Flow.LowerCapRectangle.top_lt_energyOuter_top line 54
  7. theorem OAI.SmoothLocal.Flow.LowerCapRectangle.region_subset_energyOuter line 58
  8. def OAI.SmoothLocal.Flow.LowerCapRectangle.margin line 66
  9. theorem OAI.SmoothLocal.Flow.LowerCapRectangle.margin_pos line 69
  10. theorem OAI.SmoothLocal.Flow.LowerCapRectangle.margin_bounds line 77
  11. def OAI.SmoothLocal.Flow.LowerCapRectangle.expand line 86
  12. theorem OAI.SmoothLocal.Flow.LowerCapRectangle.region_subset_expand line 99
  13. theorem OAI.SmoothLocal.Flow.LowerCapRectangle.expand_shrink_region line 106
  14. theorem OAI.SmoothLocal.Flow.LowerCapRectangle.image_subset_energyOuter line 112
  15. theorem OAI.SmoothLocal.Flow.LowerCapRectangle.image_subset_expand line 115
  16. theorem OAI.SmoothLocal.Flow.coordinateL2Bound_to_expanded_cap_coordinateBound line 122