OAI/Geometry/RecorderBoxes/Boxes.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Filled prefix rectangles and normalized separation gaps.

  1. structure OAI.Solenoidal.Bridge.Rectangle line 10
  2. def OAI.Solenoidal.Bridge.Rectangle.carrier line 14
  3. def OAI.Solenoidal.Bridge.Rectangle.SeparatedBy line 18
  4. def OAI.Solenoidal.Bridge.Rectangle.InUnit line 22
  5. theorem OAI.Solenoidal.Bridge.Rectangle.gap_mono line 26
  6. theorem OAI.Solenoidal.Bridge.Rectangle.disjoint_of_gap line 36
  7. def OAI.Solenoidal.Bridge.sourceBox line 47
  8. def OAI.Solenoidal.Bridge.targetBox line 51
  9. theorem OAI.Solenoidal.Bridge.sourceBox_carrier line 58
  10. theorem OAI.Solenoidal.Bridge.targetBox_carrier line 61
  11. theorem OAI.Solenoidal.Bridge.first_bounds line 65
  12. theorem OAI.Solenoidal.Bridge.two_bounds line 71
  13. theorem OAI.Solenoidal.Bridge.source_in_unit line 81
  14. theorem OAI.Solenoidal.Bridge.target_in_unit line 85
  15. theorem OAI.Solenoidal.Bridge.inverse_square_le_inverse line 94
  16. theorem OAI.Solenoidal.Bridge.normalized_source_gap line 100
  17. theorem OAI.Solenoidal.Bridge.normalized_target_gap line 110