Basic

📁 Source: Mathlib/Analysis/Convex/Cone/Basic.lean

Statistics

Metric	Count
Definitions ProperCone, comap, instCoePointedCone, instPartialOrder, instSetLike, map, positive, toPointedCone	8
Theorems of_nonempty_of_isClosed, canLift, coe_bot, coe_comap, coe_map, coe_positive, comap_comap, comap_id, convex, ext, ext_iff, isClosed, map_id, mem_bot, mem_comap, mem_map, mem_positive, mem_toPointedCone, nonempty, pointed_toConvexCone, smul_mem, toPointedCone_bot, toPointedCone_injective, toPointedCone_positive	24
Total	32

ConvexCone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canLift 📖	mathematical	—	CanLift ConvexCone DivisionSemiring.toSemiring Semifield.toDivisionSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ProperCone PointedCone.toConvexCone ProperCone.toPointedCone Set.Nonempty SetLike.coe instSetLike IsClosed	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Pointed.of_nonempty_of_isClosed

ConvexCone.Pointed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_nonempty_of_isClosed 📖	mathematical	Set.Nonempty SetLike.coe ConvexCone DivisionSemiring.toSemiring Semifield.toDivisionSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ConvexCone.instSetLike	ConvexCone.Pointed	—	IsClosed.closure_subset_iff ConvexCone.smul_mem ContinuousAt.continuousWithinAt ContinuousAt.smul continuousAt_id' continuousAt_const zero_smul ContinuousWithinAt.mem_closure_image closure_Ioi

ProperCone

Definitions

Name	Category	Theorems
comap 📖	CompOp	6 math math: innerDual_singleton, coe_comap, dual_singleton, mem_comap, comap_comap, comap_id
instCoePointedCone 📖	CompOp	—
instPartialOrder 📖	CompOp	2 math math: innerDual_le_innerDual, dual_le_dual
instSetLike 📖	CompOp	18 math math: convex, mem_map, coe_bot, mem_dual, nonempty, subset_dual_dual, isClosed, coe_comap, relative_hyperplane_separation, ext_iff, dual_flip_dual, dual_dual_flip, mem_innerDual, mem_bot, mem_comap, mem_positive, mem_toPointedCone, innerDual_innerDual
map 📖	CompOp	4 math math: mem_map, map_id, relative_hyperplane_separation, coe_map
positive 📖	CompOp	5 math math: coe_positive, innerDual_singleton, dual_singleton, toPointedCone_positive, mem_positive
toPointedCone 📖	CompOp	8 math math: ConvexCone.canLift, mem_map, toPointedCone_bot, coe_map, toPointedCone_injective, toPointedCone_positive, pointed_toConvexCone, mem_toPointedCone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_bot 📖	mathematical	—	SetLike.coe ProperCone instSetLike Bot.bot OrderBot.toBot Preorder.toLE ClosedSubmodule PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule ClosedSubmodule.instPartialOrder ClosedSubmodule.instOrderBot Set Set.instSingletonSet AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
coe_comap 📖	mathematical	—	SetLike.coe ProperCone instSetLike comap Set.preimage DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	—
coe_map 📖	mathematical	—	toPointedCone map PointedCone.closure PointedCone.map ContinuousLinearMap.toLinearMap RingHom.id Semiring.toNonAssocSemiring	—	—
coe_positive 📖	mathematical	—	SetLike.coe ClosedSubmodule Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule ClosedSubmodule.instSetLike positive Set.Ici AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
comap_comap 📖	mathematical	—	comap ContinuousLinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
comap_id 📖	mathematical	—	comap ContinuousLinearMap.id	—	—
convex 📖	mathematical	—	Convex SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SetLike.coe ProperCone instSetLike	—	PointedCone.convex
ext 📖	—	ProperCone SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	ProperCone SetLike.instMembership instSetLike	—	ext
isClosed 📖	mathematical	—	IsClosed SetLike.coe ProperCone instSetLike	—	ClosedSubmodule.isClosed' IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
map_id 📖	mathematical	—	map ContinuousLinearMap.id	—	ClosedSubmodule.map_id IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
mem_bot 📖	mathematical	—	ProperCone SetLike.instMembership instSetLike Bot.bot OrderBot.toBot Preorder.toLE ClosedSubmodule PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule ClosedSubmodule.instPartialOrder ClosedSubmodule.instOrderBot AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
mem_comap 📖	mathematical	—	ProperCone SetLike.instMembership instSetLike comap DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.funLike	—	—
mem_map 📖	mathematical	—	ProperCone SetLike.instMembership instSetLike map PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule PointedCone.closure PointedCone.map ContinuousLinearMap.toLinearMap RingHom.id toPointedCone	—	—
mem_positive 📖	mathematical	—	ProperCone SetLike.instMembership instSetLike positive Preorder.toLE PartialOrder.toPreorder AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
mem_toPointedCone 📖	mathematical	—	PointedCone SetLike.instMembership Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule toPointedCone ProperCone instSetLike	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
nonempty 📖	mathematical	—	Set.Nonempty SetLike.coe ProperCone instSetLike	—	Submodule.nonempty IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
pointed_toConvexCone 📖	mathematical	—	ConvexCone.Pointed SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PointedCone.toConvexCone toPointedCone	—	PointedCone.pointed_toConvexCone
smul_mem 📖	mathematical	ProperCone SetLike.instMembership instSetLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Submodule.smul_mem IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
toPointedCone_bot 📖	mathematical	—	toPointedCone Bot.bot ProperCone OrderBot.toBot Preorder.toLE ClosedSubmodule PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule ClosedSubmodule.instPartialOrder ClosedSubmodule.instOrderBot PointedCone Submodule.instBot	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
toPointedCone_injective 📖	mathematical	—	ProperCone PointedCone toPointedCone	—	ClosedSubmodule.toSubmodule_injective IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
toPointedCone_positive 📖	mathematical	—	toPointedCone positive PointedCone.positive	—	—

(root)

Definitions

Name	Category	Theorems
ProperCone 📖	CompOp	37 math math: ProperCone.dual_insert, ProperCone.innerDual_le_innerDual, ProperCone.dual_sUnion, ProperCone.convex, ConvexCone.canLift, ProperCone.innerDual_univ, ProperCone.mem_map, ProperCone.coe_bot, ProperCone.mem_dual, ProperCone.innerDual_sUnion, ProperCone.nonempty, ProperCone.subset_dual_dual, ProperCone.innerDual_zero, ProperCone.isClosed, ProperCone.dual_univ, ProperCone.coe_comap, ProperCone.dual_iUnion, ProperCone.innerDual_union, ProperCone.dual_zero, ProperCone.relative_hyperplane_separation, ProperCone.ext_iff, ProperCone.innerDual_insert, ProperCone.dual_flip_dual, ProperCone.toPointedCone_bot, ProperCone.innerDual_empty, ProperCone.dual_dual_flip, ProperCone.toPointedCone_injective, ProperCone.mem_innerDual, ProperCone.mem_bot, ProperCone.dual_empty, ProperCone.mem_comap, ProperCone.dual_le_dual, ProperCone.mem_positive, ProperCone.dual_union, ProperCone.innerDual_iUnion, ProperCone.mem_toPointedCone, ProperCone.innerDual_innerDual

---

← Back to Index