OAI/Geometry/ProjectionBody/Specification.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.ProjectionCounterexample.Specification.product_is_convex_bodyline 10 - theorem
OAI.ProjectionCounterexample.Specification.projection_support_attainedline 12 - theorem
OAI.ProjectionCounterexample.Specification.simplex_ratioline 22 - theorem
OAI.ProjectionCounterexample.Specification.product_ratioline 26 - theorem
OAI.ProjectionCounterexample.Specification.simplex_upper_bound_falseline 34