Theorem ProperCone.mem_positive

Modification history

2025-06-12 10:35

Mathlib/Analysis/Convex/Cone/Basic.lean

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

Modified ProperCone.mem_positive View on Github →

2023-07-24 10:54

Mathlib/Analysis/Convex/Cone/Proper.lean

feat(Analysis/Convex/Cone/Proper): define ProperCone.positive extending ConvexCone.positive (#6059) …

Added ProperCone.mem_positive View on Github →