OAI/Geometry/CylinderCovering/Ruled/Projection.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RuledApproximation.perpendicularProjectionEquiv line 10
  2. theorem OAI.RuledApproximation.perpendicularProjectionEquiv_apply line 19
  3. lemma OAI.RuledApproximation.projectedCylinder_base_measurable line 22
  4. lemma OAI.RuledApproximation.projectedCylinder_base_bounded line 27
  5. lemma OAI.RuledApproximation.projectedCylinder_base_open line 32
  6. lemma OAI.RuledApproximation.projectedCylinder_base_compact line 36
  7. def OAI.RuledApproximation.Cylinder.transport line 40
  8. lemma OAI.RuledApproximation.Cylinder.transport_carrier line 43
  9. lemma OAI.RuledApproximation.Cylinder.transport_area line 50
  10. lemma OAI.RuledApproximation.Cylinder.transport_parallelogram line 54
  11. def OAI.RuledApproximation.Cylinder.transportBase line 58
  12. lemma OAI.RuledApproximation.Cylinder.transport_base line 64
  13. lemma OAI.RuledApproximation.Cylinder.transport_measurable line 70
  14. lemma OAI.RuledApproximation.Cylinder.transport_bounded line 75
  15. lemma OAI.RuledApproximation.Cylinder.transport_open line 80
  16. lemma OAI.RuledApproximation.Cylinder.transport_compact line 85
  17. theorem OAI.RuledApproximation.physicalProjection_proof line 90