Commit 2023-07-03 06:43 3d8581ea

View on Github →

fix: re-port Mathlib.Analysis.Convex.Cone.Proper (#5646) Forward port [#19008](https://github.com/leanprover-community/mathlib/pull/19008) When I ported this file (Mathlib/Analysis/Convex/Cone/Proper.lean) I did not realize that mathport had used an older commit without the latest PR. I'm forward porting it now.

Estimated changes

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

added theorem ProperCone.coe_comap

added theorem ProperCone.comap_comap

added theorem ProperCone.comap_id

added theorem ProperCone.hyperplane_separation

added theorem ProperCone.hyperplane_separation_of_nmem

added theorem ProperCone.mem_comap