mathlib3
cad35c79 - feat(analysis/convex/cone): add `convex_cone.strictly_positive` and monotonicity lemmas (#15837)

Commit
3 years ago
feat(analysis/convex/cone): add `convex_cone.strictly_positive` and monotonicity lemmas (#15837) The monotonicity lemmas transfer `poined`, `blunt`, `salient`, and `flat` across inequalities of cones. This also renames `convex_cone.positive_cone` to `convex_cone.positive` to reduce duplication.
Author
Parents
Loading