Theorem ProperCone.mem_toPointedCone

Modification history

2026-01-17 20:29

Mathlib/Analysis/Convex/Cone/Basic.lean

feat(Analysis/InnerProductSpace/Orthogonal): add duplicates for `ClosedSubmodule` (#29241) …

Modified ProperCone.mem_toPointedCone View on Github →

2025-06-12 10:35

Mathlib/Analysis/Convex/Cone/Basic.lean

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

Added ProperCone.mem_toPointedCone View on Github →