OAI/Geometry/CylinderCovering/Beams/BeamStrip.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CylinderCovering.BeamStrip.denominator_pos line 10
  2. lemma OAI.CylinderCovering.BeamStrip.denominator_sq line 14
  3. lemma OAI.CylinderCovering.BeamStrip.inner_vec line 19
  4. lemma OAI.CylinderCovering.BeamStrip.norm_vec_sq line 24
  5. lemma OAI.CylinderCovering.BeamStrip.normal_norm line 28
  6. lemma OAI.CylinderCovering.BeamStrip.axis_norm line 37
  7. lemma OAI.CylinderCovering.BeamStrip.normal_axis_inner line 46
  8. lemma OAI.CylinderCovering.BeamStrip.axis_vertical_inner line 50
  9. lemma OAI.CylinderCovering.BeamStrip.normal_vertical_inner line 54
  10. lemma OAI.CylinderCovering.BeamStrip.vertical_norm line 58
  11. lemma OAI.CylinderCovering.BeamStrip.rectangle_perpendicular line 62
  12. lemma OAI.CylinderCovering.BeamStrip.rectangle_compact line 69
  13. lemma OAI.CylinderCovering.BeamStrip.IsHorizontalRectangle.isCompact line 82
  14. lemma OAI.CylinderCovering.BeamStrip.IsHorizontalRectangle.measurableSet line 88
  15. lemma OAI.CylinderCovering.BeamStrip.IsHorizontalRectangle.finite_volume line 91
  16. def OAI.CylinderCovering.BeamStrip.frameLinear line 94
  17. lemma OAI.CylinderCovering.BeamStrip.frame_inner line 99
  18. def OAI.CylinderCovering.BeamStrip.frame line 110
  19. def OAI.CylinderCovering.BeamStrip.coordinateBox line 113
  20. def OAI.CylinderCovering.BeamStrip.planeBox line 116
  21. lemma OAI.CylinderCovering.BeamStrip.rectangle_image line 118
  22. lemma OAI.CylinderCovering.BeamStrip.planeBox_volume line 129
  23. lemma OAI.CylinderCovering.BeamStrip.rectangle_area line 148
  24. lemma OAI.CylinderCovering.BeamStrip.frame_mem_perpendicular line 159
  25. def OAI.CylinderCovering.BeamStrip.perpendicularFrame line 167
  26. def OAI.CylinderCovering.BeamStrip.rectangleCylinder line 172
  27. lemma OAI.CylinderCovering.BeamStrip.rectangleCylinder_base_image line 177
  28. lemma OAI.CylinderCovering.BeamStrip.rectangleCylinder_shape line 185
  29. lemma OAI.CylinderCovering.BeamStrip.rectangleCylinder_carrier line 189
  30. lemma OAI.CylinderCovering.BeamStrip.perpendicular_finrank line 202
  31. lemma OAI.CylinderCovering.BeamStrip.rectangleCylinder_area line 212
  32. lemma OAI.CylinderCovering.BeamStrip.rectangleCylinder_compact line 229
  33. lemma OAI.CylinderCovering.BeamStrip.denominator_ge_one line 234
  34. lemma OAI.CylinderCovering.BeamStrip.coordinate_decomposition line 239
  35. lemma OAI.CylinderCovering.BeamStrip.mem_cylinder_of_frozen_bound line 251
  36. lemma OAI.CylinderCovering.BeamStrip.frozen_scalar_bound line 259
  37. lemma OAI.CylinderCovering.BeamStrip.frozen_rectangle_covers line 278