Commit 2023-09-29 03:32 f7069483

View on Github →

feat(Analysis): define pointed cones (#6437) We define PointedCone as Submodule 𝕜≥0 E. Most of this code is copied from the ConvexCone file. The main reason for this type synonym is to be able to work with direct sums/products of cones (which are now just direct sums/products of submodules).

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Nonneg/Module.lean

added theorem Nonneg.coe_smul

added theorem Nonneg.mk_smul

Modified Mathlib/Analysis/Convex/Cone/Basic.lean

added theorem ConvexCone.coe_map

Created Mathlib/Analysis/Convex/Cone/Pointed.lean

added theorem ConvexCone.coe_toPointedCone

added theorem ConvexCone.mem_toPointedCone

added def ConvexCone.toPointedCone

added theorem PointedCone.coe_comap

added theorem PointedCone.coe_map

added def PointedCone.comap

added theorem PointedCone.comap_comap

added theorem PointedCone.comap_id

added def PointedCone.dual

added theorem PointedCone.ext

added def PointedCone.map

added theorem PointedCone.map_id

added theorem PointedCone.map_map

added theorem PointedCone.mem_comap

added theorem PointedCone.mem_dual

added theorem PointedCone.mem_map

added theorem PointedCone.mem_positive

added def PointedCone.positive

added def PointedCone.toConvexCone

added theorem PointedCone.toConvexCone_dual

added theorem PointedCone.toConvexCone_injective

added theorem PointedCone.toConvexCone_map

added theorem PointedCone.toConvexCone_pointed

added theorem PointedCone.toConvexCone_positive