OAI/Analysis/LipschitzHilbert/Geometry/VerticalRectangle.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Vertical Euclidean enclosures of fat slope parallelograms. The constant vertical field makes every such enclosure Lacey--Li admissible.

  1. def OAI.LipschitzHilbert.verticalAxes line 14
  2. theorem OAI.LipschitzHilbert.verticalAxes_repr_zero line 17
  3. theorem OAI.LipschitzHilbert.verticalAxes_repr_one line 21
  4. def OAI.LipschitzHilbert.verticalRectangle line 25
  5. theorem OAI.LipschitzHilbert.mem_verticalRectangle line 34
  6. theorem OAI.LipschitzHilbert.volume_verticalRectangle_le line 50
  7. theorem OAI.LipschitzHilbert.constant_axis_popular line 62
  8. theorem OAI.LipschitzHilbert.constant_axis_admissible line 69
  9. theorem OAI.LipschitzHilbert.verticalRectangle_admissible line 76