OAI/Geometry/TranslativeCovering/BlockGeometry.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BlockGeometry.radius line 25
  2. lemma OAI.BlockGeometry.radius_nonneg line 28
  3. lemma OAI.BlockGeometry.radius_le line 38
  4. lemma OAI.BlockGeometry.exists_center line 45
  5. lemma OAI.BlockGeometry.radius_singleton line 53
  6. lemma OAI.BlockGeometry.anchor_distance line 58
  7. def OAI.BlockGeometry.loss line 72
  8. lemma OAI.BlockGeometry.loss_nonneg line 75
  9. lemma OAI.BlockGeometry.radius_le_loss line 86
  10. lemma OAI.BlockGeometry.loss_singleton line 101
  11. lemma OAI.BlockGeometry.exists_terminal line 104
  12. lemma OAI.BlockGeometry.nearby_union_radius line 115