OAI/Geometry/CylinderCovering/Beams/ProjectionFactor.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ShortenedBeam.ProjectionFactor.cycle_direction line 17
  2. lemma OAI.ShortenedBeam.ProjectionFactor.cycle_axis line 22
  3. lemma OAI.ShortenedBeam.ProjectionFactor.axis_unit line 26
  4. lemma OAI.ShortenedBeam.ProjectionFactor.direction_ne_zero line 29
  5. lemma OAI.ShortenedBeam.ProjectionFactor.horizontal_eq_map line 33
  6. lemma OAI.ShortenedBeam.ProjectionFactor.base_eq_map line 38
  7. lemma OAI.ShortenedBeam.ProjectionFactor.physicalDirection_norm line 53
  8. lemma OAI.ShortenedBeam.ProjectionFactor.raw_projection_area line 61
  9. theorem OAI.ShortenedBeam.ProjectionFactor.area line 73
  10. theorem OAI.ShortenedBeam.ProjectionFactor.base_compact line 83
  11. theorem OAI.ShortenedBeam.ProjectionFactor.base_perpendicular line 90
  12. theorem OAI.ShortenedBeam.ProjectionFactor.base_finite line 94
  13. lemma OAI.ShortenedBeam.ProjectionFactor.horizontal_physical line 103
  14. theorem OAI.ShortenedBeam.ProjectionFactor.carrier_eq line 108
  15. theorem OAI.ShortenedBeam.ProjectionFactor.normalized_area line 122
  16. theorem OAI.ShortenedBeam.ProjectionFactor.statement line 134