Commit 2024-01-09 16:50 43466302

View on Github →

refactor(ProperCone): redefine ProperCone using PointedCone (#8878) We change the definition of a ProperCone from being a nonempty, closed, ConvexCone to a closed, PointedCone. This is mathematically (not definitionally) equivalent to the earlier definition as a PointedCone is mathematically (not definitionally) the same as a nonempty, ConvexCone. The definition of PointedCone was added after ProperCone. Hence, needed to go back and update the definition.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Cone/Closure.lean

added theorem ConvexCone.closure_eq

added theorem ConvexCone.coe_closure

added theorem PointedCone.closure_eq

added theorem PointedCone.coe_closure

added theorem PointedCone.toConvexCone_closure_pointed

Modified Mathlib/Analysis/Convex/Cone/Pointed.lean

Modified Mathlib/Analysis/Convex/Cone/Proper.lean

deleted theorem ConvexCone.closure_eq

deleted theorem ConvexCone.coe_closure

modified theorem ProperCone.coe_dual

deleted theorem ProperCone.ext'

modified theorem ProperCone.mem_coe

modified theorem ProperCone.pointed_zero

added theorem ProperCone.toPointedCone_injective