OAI/Geometry/RuledCovering/Projection.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RuledApproximation.vec2_apply_zero line 12
  2. lemma OAI.RuledApproximation.vec2_apply_one line 13
  3. lemma OAI.RuledApproximation.vec3_apply_zero line 14
  4. lemma OAI.RuledApproximation.vec3_apply_one line 15
  5. lemma OAI.RuledApproximation.vec3_apply_two line 16
  6. lemma OAI.RuledApproximation.inner_vec3 line 18
  7. lemma OAI.RuledApproximation.norm_vec3_sq line 23
  8. def OAI.RuledApproximation.planeEmbedding line 28

    Source documentation

    The transverse plane in the physical normalization.

    def planeEmbedding (h : ℝ) : Plane →ₗ[ℝ] Space where
…

    Mentions: OAI.RuledApproximation.Plane, OAI.RuledApproximation.Space

  9. lemma OAI.RuledApproximation.planeEmbedding_apply line 33
  10. def OAI.RuledApproximation.physicalDirection line 36
  11. lemma OAI.RuledApproximation.physicalDirection_ne_zero line 38
  12. lemma OAI.RuledApproximation.physicalDirection_norm_sq line 43
  13. lemma OAI.RuledApproximation.physicalDirection_norm_pos line 48
  14. def OAI.RuledApproximation.physicalUnit line 51
  15. lemma OAI.RuledApproximation.physicalUnit_norm line 54
  16. def OAI.RuledApproximation.rawProjection line 58
  17. lemma OAI.RuledApproximation.rawProjection_mem line 66
  18. def OAI.RuledApproximation.perpendicularProjection line 76
  19. lemma OAI.RuledApproximation.inner_rawProjection line 80
  20. lemma OAI.RuledApproximation.rawProjection_normDet_sq line 94
  21. lemma OAI.RuledApproximation.rawProjection_normDet line 111
  22. lemma OAI.RuledApproximation.physicalWeight_eq_inv_norm line 120
  23. lemma OAI.RuledApproximation.perpendicularProjection_normDet line 124
  24. lemma OAI.RuledApproximation.perpendicularPlane_finrank line 130
  25. lemma OAI.RuledApproximation.perpendicularProjection_volume line 137
  26. lemma OAI.RuledApproximation.perpendicularProjection_injective line 151
  27. lemma OAI.RuledApproximation.IsParallelogram.linear_image line 161
  28. def OAI.RuledApproximation.projectedCylinder line 180

    Source documentation

    A genuine cylinder in its perpendicular plane, not an oblique intercept patch.

    def projectedCylinder (h : ℝ) (g : Plane) (P : Set Plane) : Cylinder where
…

    Mentions: OAI.RuledApproximation.Plane, OAI.RuledApproximation.Cylinder

  29. lemma OAI.RuledApproximation.projectedCylinder_area line 185
  30. lemma OAI.RuledApproximation.projectedCylinder_parallelogram line 190
  31. lemma OAI.RuledApproximation.projectedCylinder_mem_iff line 195
  32. lemma OAI.RuledApproximation.projectedCylinder_carrier line 221
  33. lemma OAI.RuledApproximation.physicalRuled_mem_projectedCylinder line 237