OAI/Geometry/TranslativeCovering/CylinderVolume.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CylinderVolume.scale line 37
  2. lemma OAI.CylinderVolume.scale_apply line 39
  3. lemma OAI.CylinderVolume.scale_det line 42
  4. lemma OAI.CylinderVolume.scale_norm_sq line 55
  5. lemma OAI.CylinderVolume.scale_inverse line 70
  6. def OAI.CylinderVolume.cylinder line 76
  7. lemma OAI.CylinderVolume.cylinder_closed line 79
  8. lemma OAI.CylinderVolume.cylinder_subset_image line 84
  9. lemma OAI.CylinderVolume.cylinder_volume line 104
  10. lemma OAI.CylinderVolume.perp_sq line 132
  11. lemma OAI.CylinderVolume.cylinder_translated_volume line 137
  12. lemma OAI.CylinderVolume.affine_cylinder_volume line 157