Pointed

📁 Source: Mathlib/Geometry/Convex/Cone/Pointed.lean

Statistics

Metric	Count
Definitions Pointed, toPointedCone, Pointed, PointedCone, comap, hull, instCoeConvexCone, instCoeSubmodule, lineal, map, ofConeComb, ofSubmodule, ofSubmoduleEmbedding, ofSubmoduleLatticeHom, positive, toConvexCone, Pointed	17
Theorems coe_toPointedCone, mem_toPointedCone, toPointedCone_top, coe_comap, coe_lineal, coe_map, coe_ofConeComb, coe_ofSubmodule, comap_comap, comap_id, convex, ext, ext_iff, gc_ofSubmodule_lineal, instCanLiftConvexConeToConvexConePointed, lineal_eq_sSup, lineal_le, map_id, map_map, mem_comap, mem_hull_set, mem_lineal, mem_map, mem_ofSubmodule_iff, mem_positive, mem_span_set, mem_toConvexCone, ofSubmodule_iInf, ofSubmodule_iSup, ofSubmodule_inf, ofSubmodule_inj, ofSubmodule_lineal, ofSubmodule_sInf, ofSubmodule_sSup, ofSubmodule_sup, pointed_toConvexCone, salient_iff_inter_neg_eq_singleton, smul_mem, subset_hull, subset_span, support_eq, toConvexCone_injective, toConvexCone_map, toConvexCone_positive, to_isOrderedModule	45
Total	62

ConvexCone

Definitions

Name	Category	Theorems
Pointed 📖	MathDef	12 math math: PointedCone.toConvexCone_closure_pointed, Pointed.mono, pointed_positive, PointedCone.pointed_toConvexCone, Flat.pointed, pointed_iff_not_blunt, pointed_zero, Submodule.pointed_toConvexCone, ProperCone.pointed_toConvexCone, Pointed.of_nonempty_of_isClosed, blunt_iff_not_pointed, PointedCone.instCanLiftConvexConeToConvexConePointed
toPointedCone 📖	CompOp	3 math math: coe_toPointedCone, toPointedCone_top, mem_toPointedCone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toPointedCone 📖	mathematical	Pointed SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	PointedCone.toConvexCone toPointedCone	—	—
mem_toPointedCone 📖	mathematical	Pointed SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	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 ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instSetLike	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
toPointedCone_top 📖	mathematical	—	toPointedCone Top.top ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder PointedCone Submodule.instTop MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	—

PointedCone

Definitions

Name	Category	Theorems
comap 📖	CompOp	6 math math: comap_comap, comap_id, mem_comap, dual_eq_comap_dual_eval, coe_comap, dual_singleton
hull 📖	CompOp	7 math math: dual_hull, subset_hull, subset_span, mem_span_set, mem_hull_set, IsSimplicial.hull, dual_span
instCoeConvexCone 📖	CompOp	—
instCoeSubmodule 📖	CompOp	—
lineal 📖	CompOp	7 math math: ofSubmodule_lineal, lineal_eq_sSup, coe_lineal, gc_ofSubmodule_lineal, support_eq, lineal_le, mem_lineal
map 📖	CompOp	12 math math: map_id, ProperCone.mem_map, coe_map, map_map, maxTensorProduct_map_le, mem_map, ProperCone.coe_map, minTensorProduct_comm, minTensorProduct_map_le, maxTensorProduct_comm, toConvexCone_map, dual_eq_dual_id_map
ofConeComb 📖	CompOp	1 math math: coe_ofConeComb
ofSubmodule 📖	CompOp	13 math math: ofSubmodule_lineal, ofSubmodule_sSup, coe_ofSubmodule, ofSubmodule_inj, ofSubmodule_sInf, lineal_eq_sSup, gc_ofSubmodule_lineal, ofSubmodule_iSup, ofSubmodule_inf, mem_ofSubmodule_iff, ofSubmodule_sup, ofSubmodule_iInf, lineal_le
ofSubmoduleEmbedding 📖	CompOp	—
ofSubmoduleLatticeHom 📖	CompOp	—
positive 📖	CompOp	4 math math: ProperCone.toPointedCone_positive, mem_positive, toConvexCone_positive, dual_singleton
toConvexCone 📖	CompOp	11 math math: toConvexCone_closure_pointed, ConvexCone.canLift, ConvexCone.coe_toPointedCone, pointed_toConvexCone, toConvexCone_map, ProperCone.pointed_toConvexCone, mem_toConvexCone, instCanLiftConvexConeToConvexConePointed, toConvexCone_positive, salient_iff_inter_neg_eq_singleton, toConvexCone_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comap 📖	mathematical	—	SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule comap Set.preimage DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
coe_lineal 📖	mathematical	—	SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.setLike lineal Set Set.instInter Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring Nonneg.instModule Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid AddCommGroup.toAddGroup	—	—
coe_map 📖	mathematical	—	SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule map Set.image DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
coe_ofConeComb 📖	mathematical	Set.Nonempty Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	SetLike.coe Submodule Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule Submodule.setLike ofConeComb	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
coe_ofSubmodule 📖	mathematical	—	SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule ofSubmodule Submodule	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
comap_comap 📖	mathematical	—	comap LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	—
comap_id 📖	mathematical	—	comap LinearMap.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 PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	ConvexCone.convex
ext 📖	—	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	—	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono SetLike.ext
ext_iff 📖	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	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono ext
gc_ofSubmodule_lineal 📖	mathematical	—	GaloisConnection Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid PointedCone SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder PartialOrder.toPreorder Submodule.instPartialOrder Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule ofSubmodule lineal	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass
instCanLiftConvexConeToConvexConePointed 📖	mathematical	—	CanLift ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PointedCone toConvexCone ConvexCone.Pointed	—	—
lineal_eq_sSup 📖	mathematical	—	lineal SupSet.sSup Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice setOf PointedCone SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule ofSubmodule	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono GaloisConnection.le_iff_le gc_ofSubmodule_lineal csSup_Iic
lineal_le 📖	mathematical	—	PointedCone Ring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule ofSubmodule lineal	—	GaloisConnection.l_u_le IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono gc_ofSubmodule_lineal
map_id 📖	mathematical	—	map LinearMap.id	—	SetLike.coe_injective IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Set.image_id
map_map 📖	mathematical	—	map LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	SetLike.coe_injective IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono RingHomCompTriple.ids Set.image_image
mem_comap 📖	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 comap DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
mem_hull_set 📖	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 hull Finsupp Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finsupp.support DFunLike.coe Finsupp.instFunLike Finsupp.sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Submodule.mem_span_set
mem_lineal 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike lineal PointedCone SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
mem_map 📖	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 map DFunLike.coe LinearMap RingHom.id LinearMap.instFunLike	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
mem_ofSubmodule_iff 📖	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 ofSubmodule Submodule	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
mem_positive 📖	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 positive AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
mem_span_set 📖	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 hull Finsupp Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finsupp.support DFunLike.coe Finsupp.instFunLike Finsupp.sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	mem_hull_set
mem_toConvexCone 📖	mathematical	—	ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SetLike.instMembership ConvexCone.instSetLike toConvexCone PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	—
ofSubmodule_iInf 📖	mathematical	—	ofSubmodule iInf Submodule Submodule.instInfSet Set Set.instMembership PointedCone Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono sInf_eq_iInf ofSubmodule_sInf iInf_image
ofSubmodule_iSup 📖	mathematical	—	ofSubmodule iSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set Set.instMembership PointedCone Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono sSup_eq_iSup ofSubmodule_sSup iSup_image
ofSubmodule_inf 📖	mathematical	—	ofSubmodule Submodule Submodule.instMin PointedCone Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Submodule.restrictScalars_inf IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
ofSubmodule_inj 📖	mathematical	—	ofSubmodule	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
ofSubmodule_lineal 📖	mathematical	—	ofSubmodule Ring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid lineal PointedCone Submodule.instMin Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule Submodule.pointwiseNeg	—	—
ofSubmodule_sInf 📖	mathematical	—	ofSubmodule InfSet.sInf Submodule Submodule.instInfSet PointedCone Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule Set.image	—	sInfHom.map_sInf' IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
ofSubmodule_sSup 📖	mathematical	—	ofSubmodule SupSet.sSup Submodule ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice PointedCone Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule Set.image	—	CompleteLatticeHom.map_sSup' IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
ofSubmodule_sup 📖	mathematical	—	ofSubmodule Submodule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice PointedCone Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Submodule.restrictScalars_sup 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 toConvexCone	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass
salient_iff_inter_neg_eq_singleton 📖	mathematical	—	ConvexCone.Salient SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction toConvexCone Set Set.instInter SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule InvolutiveNeg.toNeg Set.involutiveNeg SubtractionMonoid.toInvolutiveNeg SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Set.instSingletonSet NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass neg_zero
smul_mem 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring PointedCone SetLike.instMembership Submodule.setLike Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	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 SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Submodule.smul_mem
subset_hull 📖	mathematical	—	Set Set.instHasSubset SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule hull	—	Submodule.subset_span IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
subset_span 📖	mathematical	—	Set Set.instHasSubset SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule hull	—	subset_hull
support_eq 📖	mathematical	—	AddSubmonoid.support AddCommGroup.toAddGroup Submodule.toAddSubmonoid Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono AddCommGroup.toAddCommMonoid Nonneg.instModule Submodule.toAddSubgroup lineal	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
toConvexCone_injective 📖	mathematical	—	PointedCone ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction toConvexCone	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
toConvexCone_map 📖	mathematical	—	toConvexCone map ConvexCone.map	—	—
toConvexCone_positive 📖	mathematical	—	toConvexCone positive ConvexCone.positive	—	—
to_isOrderedModule 📖	mathematical	Preorder.toLE PartialOrder.toPreorder PointedCone Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	IsOrderedModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono IsOrderedModule.of_smul_nonneg IsOrderedRing.toIsOrderedAddMonoid sub_zero smul_mem

Prod

Definitions

Name	Category	Theorems
Pointed 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
Pointed 📖	CompData	43 math math: partialFunToPointed_map, pointedToTwoPFst_obj_toTwoPointing_toProd, typeToPartialFunIsoPartialFunToPointed_inv_app_toFun, partialFunEquivPointed_counitIso_inv_app_toFun, pointedToBipointedFst_comp_swap, partialFunEquivPointed_unitIso_hom_app, Pointed.Hom.id_toFun', pointedToPartialFun_map, partialFunEquivPointed_unitIso_inv_app, swap_comp_bipointedToPointedFst, pointedToTwoPFst_comp_swap, typeToPointed_map_toFun, typeToPartialFunIsoPartialFunToPointed_hom_app_toFun, partialFunEquivPointed_functor_map_toFun, Pointed.Hom.comp_toFun', pointedToTwoPFst_obj_X, pointedToPartialFun_obj, pointedToTwoPFst_map_hom_toFun, pointedToTwoPFst_comp_forget_to_bipointed, pointedToBipointedCompBipointedToPointedSnd_hom_app_toFun, pointedToTwoPSnd_obj_X, partialFunEquivPointed_inverse_obj, pointedToBipointedCompBipointedToPointedSnd_inv_app_toFun, partialFunEquivPointed_functor_obj_X, pointedToBipointedCompBipointedToPointedFst_inv_app_toFun, pointedToBipointedCompBipointedToPointedFst_hom_app_toFun, Pointed.Iso.mk_inv_toFun, bipointedToPointedSnd_comp_forget, partialFunToPointed_obj, swap_comp_bipointedToPointedSnd, pointedToTwoPSnd_comp_swap, partialFunEquivPointed_inverse_map_Dom, pointedToTwoPSnd_map_hom_toFun, partialFunEquivPointed_counitIso_hom_app_toFun, partialFunEquivPointed_inverse_map_get_coe, typeToPointed_obj_X, pointedToTwoPSnd_obj_toTwoPointing_toProd, partialFunEquivPointed_functor_obj_point, typeToPointed_obj_point, Pointed.Iso.mk_hom_toFun, pointedToTwoPSnd_comp_forget_to_bipointed, pointedToBipointedSnd_comp_swap, bipointedToPointedFst_comp_forget
PointedCone 📖	CompOp	81 math math: PointedCone.ofSubmodule_lineal, PointedCone.ofSubmodule_sSup, PointedCone.coe_ofSubmodule, PointedCone.dual_sup, PointedCone.DualFG.dual_dual_flip, PointedCone.dual_hull, ProperCone.mem_map, PointedCone.maxTensorProduct_mono, PointedCone.coe_map, PointedCone.subset_dual_dual, PointedCone.subset_hull, PointedCone.dual_ker, PointedCone.DualFG.exists_fg_dual, PointedCone.dual_union, PointedCone.tmul_mem_maxTensorProduct, PointedCone.DualFG.top, PointedCone.minTensorProduct_mono, PointedCone.ofSubmodule_sInf, PointedCone.mem_dual, PointedCone.DualFG.dual_flip_dual, PointedCone.dual_empty, PointedCone.lineal_eq_sSup, PointedCone.FG.dual_dualfg, PointedCone.maxTensorProduct_map_le, PointedCone.dual_insert, PointedCone.dual_antitone, PointedCone.basis_coord_mem_dual, ConvexCone.toPointedCone_top, PointedCone.convex, PointedCone.mem_map, PointedCone.coe_closure, PointedCone.tmul_subset_maxTensorProduct, PointedCone.dual_zero, PointedCone.minTensorProduct_le_maxTensorProduct, PointedCone.gc_ofSubmodule_lineal, PointedCone.tmul_subset_minTensorProduct, PointedCone.subset_span, PointedCone.ext_iff, PointedCone.dual_iUnion, PointedCone.mem_span_set, ProperCone.toPointedCone_bot, PointedCone.ofSubmodule_iSup, PointedCone.minTensorProduct_map_le, PointedCone.ofSubmodule_inf, PointedCone.dual_le_dual, ProperCone.toPointedCone_injective, PointedCone.mem_closure, PointedCone.subset_dual_flip_iff_subset_dual, PointedCone.DualFG.inf, PointedCone.mem_comap, PointedCone.tmul_mem_minTensorProduct, PointedCone.DualFG.dual_of_fg, PointedCone.mem_toConvexCone, PointedCone.isClosed_dual, PointedCone.mem_ofSubmodule_iff, PointedCone.mem_positive, PointedCone.mem_maxTensorProduct, PointedCone.dual_singleton_zero, PointedCone.dual_neg, PointedCone.dual_flip_dual_dual_flip, ProperCone.mem_toPointedCone, PointedCone.dual_sUnion, PointedCone.mem_hull_set, PointedCone.ofSubmodule_sup, PointedCone.ofSubmodule_iInf, ConvexCone.mem_toPointedCone, PointedCone.lineal_le, PointedCone.instCanLiftConvexConeToConvexConePointed, PointedCone.closure_eq, PointedCone.dual_anti, PointedCone.smul_mem, PointedCone.DualFG.iff_exists_fg_dual, PointedCone.dual_univ, PointedCone.dual_eq_iInter_dual_singleton, PointedCone.dual_dual_flip_dual, PointedCone.coe_comap, PointedCone.dual_eq_dual_id_map, PointedCone.mem_lineal, PointedCone.salient_iff_inter_neg_eq_singleton, PointedCone.toConvexCone_injective, PointedCone.dual_span

---

← Back to Index