OAI/Geometry/TranslativeCovering/LensDeployment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LensDeployment.tangent_bad_vector line 26
2. lemma OAI.LensDeployment.projected_norm line 54
3. lemma OAI.LensDeployment.projected_bound line 62
4. lemma OAI.LensDeployment.ordinary_lens line 81
5. lemma OAI.LensDeployment.orient_axis line 136
6. lemma OAI.LensDeployment.projective_lens line 145