Commit 2023-07-01 05:11 6c3530be

View on Github →

feat: port Analysis.Convex.Cone.Proper (#5607) The remaining errors are about coe and norm_cast. I do not understand these well enough in Lean 4. Please feel free to push changes.

Estimated changes

added theorem ConvexCone.closure_eq
added theorem ConvexCone.coe_closure
added theorem ProperCone.coe_dual
added theorem ProperCone.coe_map
added theorem ProperCone.coe_zero
added def ProperCone.dual
added theorem ProperCone.dual_dual
added theorem ProperCone.ext'
added theorem ProperCone.ext
added theorem ProperCone.map_id
added theorem ProperCone.mem_coe
added theorem ProperCone.mem_dual
added theorem ProperCone.mem_map
added theorem ProperCone.mem_zero
added structure ProperCone