Theorem ProperCone.coe_comap

Modification history

2025-06-12 10:35

Mathlib/Analysis/Convex/Cone/Basic.lean

refactor: redefine `ProperCone` as an `abbrev` for `ClosedSubmodule` (#25204) …

Modified ProperCone.coe_comap View on Github →

2023-07-03 06:43

Mathlib/Analysis/Convex/Cone/Proper.lean

fix: re-port Mathlib.Analysis.Convex.Cone.Proper (#5646) …

Added ProperCone.coe_comap View on Github →