Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-10 00:22 cad35c79

View on Github →

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.

Estimated changes

Modified src/analysis/convex/cone.lean

added theorem convex_cone.blunt.anti

added theorem convex_cone.blunt_strictly_positive

added theorem convex_cone.coe_positive

added theorem convex_cone.coe_strictly_positive

added theorem convex_cone.flat.mono

added theorem convex_cone.mem_positive

added theorem convex_cone.mem_strictly_positive

added theorem convex_cone.pointed.mono

added theorem convex_cone.pointed_positive

deleted theorem convex_cone.pointed_positive_cone

added def convex_cone.positive

deleted def convex_cone.positive_cone

added theorem convex_cone.positive_le_strictly_positive

added theorem convex_cone.salient.anti

added theorem convex_cone.salient_positive

deleted theorem convex_cone.salient_positive_cone

added theorem convex_cone.salient_strictly_positive

added def convex_cone.strictly_positive