OAI/Geometry/PolarProducts/CanonicalCylinder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ConvexPolar.inner_lt_one_of_mem_interior line 14
2. theorem OAI.ConvexPolar.abs_inner_lt_one_of_mem_interior line 31
3. theorem OAI.ConvexPolar.polar_symmetric line 44
4. theorem OAI.ConvexPolar.exists_support_pair line 52
5. def OAI.SymmetricPolar.canonicalSquareCylinder line 86
6. theorem OAI.SymmetricPolar.polarProduct_subset_squareCylinder line 89
7. theorem OAI.SymmetricPolar.exists_squareCylinder line 103