OAI/Analysis/LipschitzHilbert/Geometry/FiniteTransverseDirections.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite family of transverse directions. Compactness supplies a universal net, independent of the rectangles later selected.

  1. def OAI.LipschitzHilbert.Rectangle.transverseFrame line 13
  2. theorem OAI.LipschitzHilbert.Rectangle.transverseFrame_axis line 21
  3. theorem OAI.LipschitzHilbert.Rectangle.exists_finite_transverse_directions line 24
  4. theorem OAI.LipschitzHilbert.Rectangle.transverse_coordinate_large line 47
  5. theorem OAI.LipschitzHilbert.Rectangle.nearby_transverse_coordinate line 58