OAI/Geometry/Immersion/ClosedSurface/NormalFrame.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ClosedSurfaceR4.NormalFrame.Vec line 10
2. def OAI.ClosedSurfaceR4.NormalFrame.minor3 line 12
3. def OAI.ClosedSurfaceR4.NormalFrame.perpProduct line 18
4. def OAI.ClosedSurfaceR4.NormalFrame.gramDet line 22
5. def OAI.ClosedSurfaceR4.NormalFrame.unitPerp line 24
6. lemma OAI.ClosedSurfaceR4.NormalFrame.dot_perp_left line 27
7. lemma OAI.ClosedSurfaceR4.NormalFrame.dot_perp_middle line 31
8. lemma OAI.ClosedSurfaceR4.NormalFrame.dot_perp_right line 35
9. lemma OAI.ClosedSurfaceR4.NormalFrame.perp_sq line 39
10. lemma OAI.ClosedSurfaceR4.NormalFrame.gramDet_sum_sq line 46
11. lemma OAI.ClosedSurfaceR4.NormalFrame.gramDet_nonneg line 53
12. lemma OAI.ClosedSurfaceR4.NormalFrame.gramDet_pos line 57
13. lemma OAI.ClosedSurfaceR4.NormalFrame.perp_sq_pos line 60
14. lemma OAI.ClosedSurfaceR4.NormalFrame.unitPerp_orthogonal line 70
15. lemma OAI.ClosedSurfaceR4.NormalFrame.unitPerp_unit line 75
16. lemma OAI.ClosedSurfaceR4.NormalFrame.contDiffAt_minor3 line 88
17. lemma OAI.ClosedSurfaceR4.NormalFrame.contDiffAt_perpProduct line 98
18. lemma OAI.ClosedSurfaceR4.NormalFrame.contDiffAt_unitPerp line 108