Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-29 04:30 ea177c2a

View on Github →

feat(analysis/convex): add correspondence between convex cones and ordered semimodules (#3931) This shows that a convex cone defines an ordered semimodule and vice-versa.

Estimated changes

Modified src/algebra/module/ordered.lean

Modified src/analysis/convex/cone.lean

added def convex_cone.blunt

added def convex_cone.flat

added def convex_cone.pointed

added theorem convex_cone.pointed_iff_not_blunt

added theorem convex_cone.pointed_of_positive_cone

added def convex_cone.positive_cone

added def convex_cone.salient

added theorem convex_cone.salient_iff_not_flat

added theorem convex_cone.salient_of_blunt

added theorem convex_cone.salient_of_positive_cone

added def convex_cone.to_ordered_add_comm_group

added def convex_cone.to_ordered_semimodule

added def convex_cone.to_partial_order

added def convex_cone.to_preorder