Commit 2023-05-23 07:30 22a8c45f

View on Github →

feat: port Analysis.Convex.Cone.Basic (#4152)

Estimated changes

Modified Mathlib.lean

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

added theorem Convex.mem_toCone

added theorem Convex.mem_to_cone'

added theorem Convex.subset_toCone

added def Convex.toCone

added theorem Convex.toCone_eq_sInf

added theorem Convex.toCone_isLeast

added theorem ConvexCone.Blunt.anti

added theorem ConvexCone.Blunt.salient

added def ConvexCone.Blunt

added theorem ConvexCone.Flat.mono

added theorem ConvexCone.Flat.pointed

added def ConvexCone.Flat

added theorem ConvexCone.Pointed.mono

added def ConvexCone.Pointed

added theorem ConvexCone.Salient.anti

added def ConvexCone.Salient

added theorem ConvexCone.add_mem

added theorem ConvexCone.blunt_iff_not_pointed

added theorem ConvexCone.blunt_strictlyPositive

added theorem ConvexCone.coe_bot

added theorem ConvexCone.coe_comap

added theorem ConvexCone.coe_iInf

added theorem ConvexCone.coe_inf

added theorem ConvexCone.coe_mk

added theorem ConvexCone.coe_positive

added theorem ConvexCone.coe_sInf

added theorem ConvexCone.coe_strictlyPositive

added theorem ConvexCone.coe_top

added theorem ConvexCone.coe_zero

added def ConvexCone.comap

added theorem ConvexCone.comap_comap

added theorem ConvexCone.comap_id

added theorem ConvexCone.ext

added def ConvexCone.map

added theorem ConvexCone.map_id

added theorem ConvexCone.map_map

added theorem ConvexCone.mem_add

added theorem ConvexCone.mem_bot

added theorem ConvexCone.mem_comap

added theorem ConvexCone.mem_iInf

added theorem ConvexCone.mem_inf

added theorem ConvexCone.mem_map

added theorem ConvexCone.mem_mk

added theorem ConvexCone.mem_positive

added theorem ConvexCone.mem_sInf

added theorem ConvexCone.mem_strictlyPositive

added theorem ConvexCone.mem_top

added theorem ConvexCone.mem_zero

added theorem ConvexCone.pointed_iff_not_blunt

added theorem ConvexCone.pointed_positive

added theorem ConvexCone.pointed_zero

added def ConvexCone.positive

added theorem ConvexCone.positive_le_strictlyPositive

added theorem ConvexCone.salient_iff_not_flat

added theorem ConvexCone.salient_positive

added theorem ConvexCone.salient_strictlyPositive

added theorem ConvexCone.smul_mem

added theorem ConvexCone.smul_mem_iff

added def ConvexCone.strictlyPositive

added def ConvexCone.toOrderedAddCommGroup

added def ConvexCone.toPartialOrder

added def ConvexCone.toPreorder

added theorem ConvexCone.to_orderedSMul

added structure ConvexCone

added theorem RieszExtension.exists_top

added theorem RieszExtension.step

added theorem Submodule.coe_toConvexCone

added theorem Submodule.mem_toConvexCone

added theorem Submodule.pointed_toConvexCone

added def Submodule.toConvexCone

added theorem Submodule.toConvexCone_bot

added theorem Submodule.toConvexCone_inf

added theorem Submodule.toConvexCone_le_iff

added theorem Submodule.toConvexCone_top

added theorem convexHull_toCone_eq_sInf

added theorem convexHull_toCone_isLeast

added theorem exists_extension_of_le_sublinear

added theorem riesz_extension