OAI/Geometry/RecorderBoxes/Affine.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Separated physical rectangles and their reciprocal affine maps.

  1. def OAI.Solenoidal.Bridge.sourceRectangle line 11
  2. def OAI.Solenoidal.Bridge.targetRectangle line 14
  3. theorem OAI.Solenoidal.Bridge.common_gap_le_kappa line 17
  4. theorem OAI.Solenoidal.Bridge.source_rectangles_separated line 23
  5. theorem OAI.Solenoidal.Bridge.target_rectangles_separated line 36
  6. def OAI.Solenoidal.Bridge.affine line 47
  7. theorem OAI.Solenoidal.Bridge.affine_image line 52
  8. theorem OAI.Solenoidal.Bridge.affine_linear_part line 67