OAI/Geometry/CylinderCovering/Radial/SetProjection.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RadialProjection.coordinateLinear2 line 13
  2. def OAI.RadialProjection.projectedCoordinateLinear line 20
  3. lemma OAI.RadialProjection.projectedCoordinateLinear_apply line 23
  4. lemma OAI.RadialProjection.projectedCoordinateLinear_normDet line 27
  5. lemma OAI.RadialProjection.affine_projected_image line 47
  6. theorem OAI.RadialProjection.affine_projection_measure line 58
  7. theorem OAI.RadialProjection.affine_projection_area line 71
  8. theorem OAI.RadialProjection.radial_affine_projection_area line 80
  9. theorem OAI.RadialProjection.affine_projection_finite line 89
  10. theorem OAI.RadialProjection.affine_projection_isCompact line 95