Theorem ProperCone.comap_id

Modification history

2025-06-12 10:35

Mathlib/Analysis/Convex/Cone/Basic.lean

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

Modified ProperCone.comap_id 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.comap_id View on Github →