OAI/Analysis/LipschitzHilbert/Geometry/ClippedEnclosure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The thin enclosing rectangle for an actual horizontally clipped top box. The long side is controlled by the testing strip before the published length restriction is invoked.

  1. def OAI.LipschitzHilbert.SlopeBox.thinEnclosure line 15
  2. theorem OAI.LipschitzHilbert.SlopeBox.mem_thinEnclosure line 20
  3. theorem OAI.LipschitzHilbert.SlopeBox.thinEnclosure_long_le line 28
  4. theorem OAI.LipschitzHilbert.SlopeBox.thinEnclosure_volume_le line 35
  5. theorem OAI.LipschitzHilbert.SlopeBox.clipped_aperture_ge line 45
  6. theorem OAI.LipschitzHilbert.SlopeBox.thinEnclosure_admissible line 52