OAI/GroupTheory/SimpleAmenable/Homology/ClippedLineSlide.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.coordinateRectangle_in_clippingOverlap line 14
  2. def OAI.SimpleAmenable.tangentCoefficient line 48
  3. theorem OAI.SimpleAmenable.tangentCoefficient_pos line 51
  4. theorem OAI.SimpleAmenable.tangentCoefficient_bound line 55
  5. theorem OAI.SimpleAmenable.tangentOffset_coordinate line 60
  6. def OAI.SimpleAmenable.tangentAllowedLower line 64
  7. def OAI.SimpleAmenable.tangentAllowedUpper line 69
  8. theorem OAI.SimpleAmenable.tangentAllowed_iff line 74
  9. theorem OAI.SimpleAmenable.tangentAllowed_wide line 105