Basic

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

Statistics

Metric	Count
Definitions toCone, ConvexCone, Blunt, IsGenerating, IsReproducing, Salient, carrier, comap, copy, gi, hull, instAdd, instAddCommSemigroup, instAddZeroClass, instBot, instCompleteLattice, instCompleteSemilatticeInf, instInfSet, instInhabited, instPartialOrder, instSetLike, instZero, map, positive, strictlyPositive, toPartialOrder, toPreorder, toConvexCone	28
Theorems mem_toCone, mem_toCone', subset_toCone, toCone_eq_sInf, toCone_isLeast, anti, salient, mono, pointed, isReproducing, mono, of_top_le_span, span_eq_top, top_le_span, isGenerating, of_univ_subset, sub_eq_univ, mono, anti, add_mem, add_mem', blunt_iff_not_pointed, blunt_strictlyPositive, coe_add, coe_bot, coe_comap, coe_eq_empty, coe_hull_of_convex, coe_iInf, coe_inf, coe_map, coe_mk, coe_positive, coe_sInf, coe_strictlyPositive, coe_top, coe_zero, comap_comap, comap_id, convex, copy_carrier, copy_eq, disjoint_coe, disjoint_hull_left_of_convex, disjoint_hull_right_of_convex, ext, ext_iff, gc_hull_coe, hull_le_iff, hull_min, instAddMemClass, isGenerating_bot, isGenerating_bot_iff, isGenerating_iff_isReproducing, isGenerating_top, map_id, map_map, mem_add, mem_comap, mem_hull_of_convex, mem_iInf, mem_inf, mem_map, mem_mk, mem_positive, mem_sInf, mem_strictlyPositive, mem_top, mem_zero, notMem_bot, pointed_iff_not_blunt, pointed_positive, pointed_zero, salient_iff_not_flat, salient_positive, salient_strictlyPositive, smul_mem, smul_mem', smul_mem_iff, strictlyPositive_le_positive, subset_hull, to_isOrderedAddMonoid, coe_toConvexCone, mem_toConvexCone, pointed_toConvexCone, toConvexCone_bot, toConvexCone_inf, toConvexCone_le_toConvexCone, toConvexCone_top, convexHull_toCone_eq_sInf, convexHull_toCone_isLeast	91
Total	119

Convex

Definitions

Name	Category	Theorems
toCone 📖	CompOp	7 math math: convexHull_toCone_eq_sInf, mem_toCone, toCone_isLeast, convexHull_toCone_isLeast, toCone_eq_sInf, subset_toCone, mem_toCone'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mem_toCone 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	ConvexCone SetLike.instMembership ConvexCone.instSetLike toCone Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Set Set.instMembership	—	—
mem_toCone' 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	ConvexCone SetLike.instMembership ConvexCone.instSetLike toCone Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Set Set.instMembership	—	mem_toCone inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono smul_smul inv_mul_cancel₀ LT.lt.ne' one_smul
subset_toCone 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Set Set.instHasSubset SetLike.coe ConvexCone ConvexCone.instSetLike toCone	—	mem_toCone' zero_lt_one IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero one_smul
toCone_eq_sInf 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	toCone InfSet.sInf ConvexCone ConvexCone.instInfSet setOf Set Set.instHasSubset SetLike.coe ConvexCone.instSetLike	—	IsGLB.sInf_eq IsLeast.isGLB toCone_isLeast
toCone_isLeast 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	IsLeast ConvexCone Preorder.toLE PartialOrder.toPreorder ConvexCone.instPartialOrder setOf Set Set.instHasSubset SetLike.coe ConvexCone.instSetLike toCone	—	subset_toCone mem_toCone ConvexCone.smul_mem

ConvexCone

Definitions

Name	Category	Theorems
Blunt 📖	MathDef	3 math math: blunt_strictlyPositive, pointed_iff_not_blunt, blunt_iff_not_pointed
IsGenerating 📖	MathDef	6 math math: IsReproducing.isGenerating, isGenerating_bot, IsGenerating.of_top_le_span, isGenerating_iff_isReproducing, isGenerating_top, isGenerating_bot_iff
IsReproducing 📖	MathDef	3 math math: IsGenerating.isReproducing, isGenerating_iff_isReproducing, IsReproducing.of_univ_subset
Salient 📖	MathDef	5 math math: salient_iff_not_flat, salient_strictlyPositive, Blunt.salient, salient_positive, PointedCone.salient_iff_inter_neg_eq_singleton
carrier 📖	CompOp	—
comap 📖	CompOp	4 math math: coe_comap, comap_id, comap_comap, mem_comap
copy 📖	CompOp	2 math math: copy_eq, copy_carrier
gi 📖	CompOp	—
hull 📖	CompOp	8 math math: disjoint_hull_left_of_convex, hull_min, subset_hull, disjoint_hull_right_of_convex, hull_le_iff, mem_hull_of_convex, gc_hull_coe, coe_hull_of_convex
instAdd 📖	CompOp	2 math math: mem_add, coe_add
instAddCommSemigroup 📖	CompOp	—
instAddZeroClass 📖	CompOp	—
instBot 📖	CompOp	5 math math: coe_eq_empty, notMem_bot, isGenerating_bot, isGenerating_bot_iff, coe_bot
instCompleteLattice 📖	CompOp	11 math math: Submodule.toConvexCone_inf, coe_inf, Submodule.toConvexCone_top, mem_inf, disjoint_hull_left_of_convex, toPointedCone_top, mem_top, disjoint_coe, disjoint_hull_right_of_convex, isGenerating_top, coe_top
instCompleteSemilatticeInf 📖	CompOp	—
instInfSet 📖	CompOp	6 math math: convexHull_toCone_eq_sInf, mem_iInf, coe_iInf, Convex.toCone_eq_sInf, coe_sInf, mem_sInf
instInhabited 📖	CompOp	—
instPartialOrder 📖	CompOp	10 math math: strictlyPositive_le_positive, disjoint_hull_left_of_convex, hull_min, Submodule.toConvexCone_le_toConvexCone, disjoint_coe, Convex.toCone_isLeast, convexHull_toCone_isLeast, disjoint_hull_right_of_convex, hull_le_iff, gc_hull_coe
instSetLike 📖	CompOp	55 math math: convex, mem_positive, canLift, coe_eq_empty, coe_inf, ext_iff, coe_closure, coe_zero, convexHull_toCone_eq_sInf, coe_map, coe_comap, Submodule.coe_toConvexCone, notMem_bot, mem_inf, mem_iInf, coe_strictlyPositive, mem_map, disjoint_hull_left_of_convex, mem_top, coe_mk, subset_hull, IsGenerating.top_le_span, smul_mem_iff, Convex.mem_toCone, mem_add, disjoint_coe, instAddMemClass, coe_positive, mem_mk, Convex.toCone_isLeast, mem_zero, coe_add, convexHull_toCone_isLeast, IsGenerating.span_eq_top, disjoint_hull_right_of_convex, Submodule.mem_toConvexCone, hull_le_iff, mem_strictlyPositive, mem_hull_of_convex, coe_iInf, gc_hull_coe, coe_top, PointedCone.mem_toConvexCone, Convex.toCone_eq_sInf, coe_hull_of_convex, Convex.subset_toCone, closure_eq, coe_sInf, Convex.mem_toCone', mem_toPointedCone, coe_bot, IsReproducing.sub_eq_univ, mem_closure, mem_sInf, mem_comap
instZero 📖	CompOp	4 math math: coe_zero, pointed_zero, mem_zero, Submodule.toConvexCone_bot
map 📖	CompOp	5 math math: coe_map, map_id, mem_map, PointedCone.toConvexCone_map, map_map
positive 📖	CompOp	6 math math: mem_positive, pointed_positive, strictlyPositive_le_positive, coe_positive, salient_positive, PointedCone.toConvexCone_positive
strictlyPositive 📖	CompOp	5 math math: salient_strictlyPositive, coe_strictlyPositive, strictlyPositive_le_positive, blunt_strictlyPositive, mem_strictlyPositive
toPartialOrder 📖	CompOp	1 math math: to_isOrderedAddMonoid
toPreorder 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mem 📖	mathematical	ConvexCone SetLike.instMembership instSetLike	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	add_mem'
add_mem' 📖	mathematical	Set Set.instMembership carrier	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
blunt_iff_not_pointed 📖	mathematical	—	Blunt Pointed	—	—
blunt_strictlyPositive 📖	mathematical	—	Blunt AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction strictlyPositive	—	lt_irrefl
coe_add 📖	mathematical	—	SetLike.coe ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instSetLike instAdd Set Set.add AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
coe_bot 📖	mathematical	—	SetLike.coe ConvexCone instSetLike Bot.bot instBot Set Set.instEmptyCollection	—	—
coe_comap 📖	mathematical	—	SetLike.coe ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instSetLike comap Set.preimage DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—
coe_eq_empty 📖	mathematical	—	SetLike.coe ConvexCone instSetLike Set Set.instEmptyCollection Bot.bot instBot	—	coe_bot
coe_hull_of_convex 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	SetLike.coe ConvexCone instSetLike hull setOf Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Set Set.instMembership Set.smulSet	—	Set.ext mem_hull_of_convex
coe_iInf 📖	mathematical	—	SetLike.coe ConvexCone instSetLike iInf instInfSet Set.iInter	—	Set.iInter_congr_Prop Set.iInter_exists Set.iInter_iInter_eq'
coe_inf 📖	mathematical	—	SetLike.coe ConvexCone instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice Set Set.instInter	—	—
coe_map 📖	mathematical	—	SetLike.coe ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instSetLike map Set.image DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—
coe_mk 📖	mathematical	Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	SetLike.coe ConvexCone instSetLike	—	—
coe_positive 📖	mathematical	—	SetLike.coe ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instSetLike positive Set.Ici PartialOrder.toPreorder	—	—
coe_sInf 📖	mathematical	—	SetLike.coe ConvexCone instSetLike InfSet.sInf instInfSet Set.iInter Set Set.instMembership	—	—
coe_strictlyPositive 📖	mathematical	—	SetLike.coe ConvexCone AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instSetLike strictlyPositive Set.Ioi PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_top 📖	mathematical	—	SetLike.coe ConvexCone instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder Set.univ	—	—
coe_zero 📖	mathematical	—	SetLike.coe ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instSetLike instZero Set Set.zero	—	—
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 ConvexCone instSetLike	—	convex_iff_forall_pos AddMemClass.add_mem instAddMemClass smul_mem
copy_carrier 📖	mathematical	SetLike.coe ConvexCone instSetLike	copy	—	—
copy_eq 📖	mathematical	SetLike.coe ConvexCone instSetLike	copy	—	SetLike.coe_injective
disjoint_coe 📖	mathematical	—	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe ConvexCone instSetLike instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLattice	—	—
disjoint_hull_left_of_convex 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Disjoint ConvexCone instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLattice hull Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe instSetLike	—	disjoint_coe Disjoint.mono_left subset_hull mem_hull_of_convex Iff.not smul_mem_iff
disjoint_hull_right_of_convex 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Disjoint ConvexCone instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder instCompleteLattice hull Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe instSetLike	—	disjoint_comm disjoint_hull_left_of_convex
ext 📖	—	ConvexCone SetLike.instMembership instSetLike	—	—	SetLike.ext
ext_iff 📖	mathematical	—	ConvexCone SetLike.instMembership instSetLike	—	ext
gc_hull_coe 📖	mathematical	—	GaloisConnection Set ConvexCone PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra instPartialOrder hull SetLike.coe instSetLike	—	hull_le_iff
hull_le_iff 📖	mathematical	—	ConvexCone Preorder.toLE PartialOrder.toPreorder instPartialOrder hull Set Set.instHasSubset SetLike.coe instSetLike	—	HasSubset.Subset.trans Set.instIsTransSubset subset_hull hull_min
hull_min 📖	mathematical	Set Set.instHasSubset SetLike.coe ConvexCone instSetLike	Preorder.toLE PartialOrder.toPreorder instPartialOrder hull	—	sInf_le
instAddMemClass 📖	mathematical	—	AddMemClass ConvexCone AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup instSetLike	—	add_mem'
isGenerating_bot 📖	mathematical	—	IsGenerating Bot.bot ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instBot	—	isGenerating_bot_iff
isGenerating_bot_iff 📖	mathematical	—	IsGenerating Bot.bot ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction instBot	—	Submodule.span_empty Submodule.subsingleton_iff subsingleton_iff_bot_eq_top
isGenerating_iff_isReproducing 📖	mathematical	—	IsGenerating Ring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid IsReproducing	—	IsGenerating.isReproducing IsReproducing.isGenerating
isGenerating_top 📖	mathematical	—	IsGenerating 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	—	Submodule.span_univ
map_id 📖	mathematical	—	map LinearMap.id	—	SetLike.coe_injective Set.image_id
map_map 📖	mathematical	—	map LinearMap.comp RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids	—	SetLike.coe_injective RingHomCompTriple.ids Set.image_image
mem_add 📖	mathematical	—	ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SetLike.instMembership instSetLike instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—
mem_comap 📖	mathematical	—	ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SetLike.instMembership instSetLike comap DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	—
mem_hull_of_convex 📖	mathematical	Convex DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	ConvexCone SetLike.instMembership instSetLike hull Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Set Set.instMembership Set.smulSet	—	hull_min mul_pos IsStrictOrderedRing.toPosMulStrictMono SemigroupAction.mul_smul Set.smul_mem_smul_set add_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing Convex.add_smul LT.lt.le Set.add_mem_add IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero one_smul smul_mem subset_hull
mem_iInf 📖	mathematical	—	ConvexCone SetLike.instMembership instSetLike iInf instInfSet	—	Set.mem_iInter₂
mem_inf 📖	mathematical	—	ConvexCone SetLike.instMembership instSetLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice	—	—
mem_map 📖	mathematical	—	ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SetLike.instMembership instSetLike map DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike	—	Set.mem_image
mem_mk 📖	mathematical	Set Set.instMembership AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	ConvexCone SetLike.instMembership instSetLike	—	—
mem_positive 📖	mathematical	—	ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SetLike.instMembership instSetLike positive Preorder.toLE PartialOrder.toPreorder	—	—
mem_sInf 📖	mathematical	—	ConvexCone SetLike.instMembership instSetLike InfSet.sInf instInfSet	—	Set.mem_iInter₂
mem_strictlyPositive 📖	mathematical	—	ConvexCone AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SetLike.instMembership instSetLike strictlyPositive Preorder.toLT PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
mem_top 📖	mathematical	—	ConvexCone SetLike.instMembership instSetLike Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Set.mem_univ
mem_zero 📖	mathematical	—	ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SetLike.instMembership instSetLike instZero	—	—
notMem_bot 📖	mathematical	—	ConvexCone SetLike.instMembership instSetLike Bot.bot instBot	—	—
pointed_iff_not_blunt 📖	mathematical	—	Pointed Blunt	—	—
pointed_positive 📖	mathematical	—	Pointed SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction positive	—	le_refl
pointed_zero 📖	mathematical	—	Pointed SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ConvexCone instZero	—	Pointed.eq_1 mem_zero
salient_iff_not_flat 📖	mathematical	—	Salient Flat	—	—
salient_positive 📖	mathematical	—	Salient SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction positive	—	lt_irrefl neg_add_cancel add_pos_of_nonneg_of_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono LE.le.lt_of_ne'
salient_strictlyPositive 📖	mathematical	—	Salient SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommGroup.toAddCommMonoid strictlyPositive	—	Salient.anti PosSMulStrictMono.toPosSMulMono strictlyPositive_le_positive salient_positive
smul_mem 📖	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ConvexCone SetLike.instMembership instSetLike	—	—	smul_mem'
smul_mem' 📖	—	Preorder.toLT PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Set Set.instMembership carrier	—	—	—
smul_mem_iff 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing	ConvexCone DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction SetLike.instMembership instSetLike	—	smul_mem inv_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono inv_smul_smul₀ LT.lt.ne'
strictlyPositive_le_positive 📖	mathematical	—	ConvexCone AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder strictlyPositive positive PosSMulStrictMono.toPosSMulMono MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid MulActionWithZero.toSMulWithZero Module.toMulActionWithZero	—	le_of_lt
subset_hull 📖	mathematical	—	Set Set.instHasSubset SetLike.coe ConvexCone instSetLike hull	—	—
to_isOrderedAddMonoid 📖	mathematical	Pointed AddCommGroup.toAddCommMonoid Salient	toPartialOrder	—	add_sub_add_right_eq_sub

ConvexCone.Blunt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
anti 📖	—	ConvexCone Preorder.toLE PartialOrder.toPreorder ConvexCone.instPartialOrder ConvexCone.Blunt	—	—	—
salient 📖	mathematical	ConvexCone.Blunt AddCommGroup.toAddCommMonoid	ConvexCone.Salient	—	ConvexCone.salient_iff_not_flat ConvexCone.blunt_iff_not_pointed ConvexCone.Flat.pointed

ConvexCone.Flat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	ConvexCone AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder ConvexCone.instPartialOrder ConvexCone.Flat	—	—	—
pointed 📖	mathematical	ConvexCone.Flat	ConvexCone.Pointed AddCommGroup.toAddCommMonoid	—	ConvexCone.Pointed.eq_1 add_neg_cancel AddMemClass.add_mem ConvexCone.instAddMemClass

ConvexCone.IsGenerating

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isReproducing 📖	mathematical	ConvexCone.IsGenerating Ring.toSemiring SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid	ConvexCone.IsReproducing	—	ConvexCone.IsReproducing.eq_1 Set.eq_univ_iff_forall Set.nonempty_iff_ne_empty not_subsingleton ConvexCone.isGenerating_bot_iff ConvexCone.coe_eq_empty ConvexCone.add_mem add_sub_add_comm sub_self lt_trichotomy ConvexCone.smul_mem neg_pos neg_smul neg_sub_neg smul_sub zero_smul add_sub_cancel_right Submodule.span_le
mono 📖	—	ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder ConvexCone.instPartialOrder ConvexCone.IsGenerating	—	—	eq_1 top_le_iff LE.le.trans Submodule.span_mono
of_top_le_span 📖	mathematical	Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span SetLike.coe ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ConvexCone.instSetLike	ConvexCone.IsGenerating	—	eq_top_iff
span_eq_top 📖	mathematical	ConvexCone.IsGenerating	Submodule.span SetLike.coe ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ConvexCone.instSetLike Top.top Submodule Submodule.instTop	—	—
top_le_span 📖	mathematical	ConvexCone.IsGenerating	Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span SetLike.coe ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ConvexCone.instSetLike	—	Eq.ge span_eq_top

ConvexCone.IsReproducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGenerating 📖	mathematical	ConvexCone.IsReproducing Ring.toSemiring	ConvexCone.IsGenerating AddCommGroup.toAddCommMonoid	—	ConvexCone.IsGenerating.eq_1 eq_top_iff Set.mem_sub Set.eq_univ_iff_forall eq_1 sub_mem Submodule.addSubgroupClass Submodule.subset_span
of_univ_subset 📖	mathematical	Set Set.instHasSubset Set.univ Set.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SetLike.coe ConvexCone AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ConvexCone.instSetLike	ConvexCone.IsReproducing	—	Set.eq_univ_iff_forall Set.mem_univ
sub_eq_univ 📖	mathematical	ConvexCone.IsReproducing	Set Set.sub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SetLike.coe ConvexCone AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ConvexCone.instSetLike Set.univ	—	—

ConvexCone.Pointed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	ConvexCone Preorder.toLE PartialOrder.toPreorder ConvexCone.instPartialOrder ConvexCone.Pointed	—	—	—

ConvexCone.Salient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
anti 📖	—	ConvexCone AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder ConvexCone.instPartialOrder ConvexCone.Salient	—	—	—

Submodule

Definitions

Name	Category	Theorems
toConvexCone 📖	CompOp	7 math math: toConvexCone_inf, coe_toConvexCone, toConvexCone_top, toConvexCone_le_toConvexCone, pointed_toConvexCone, mem_toConvexCone, toConvexCone_bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toConvexCone 📖	mathematical	—	SetLike.coe ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ConvexCone.instSetLike toConvexCone Submodule setLike	—	—
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 Submodule setLike	—	—
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	—	zero_mem
toConvexCone_bot 📖	mathematical	—	toConvexCone Bot.bot Submodule instBot ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ConvexCone.instZero	—	—
toConvexCone_inf 📖	mathematical	—	toConvexCone Submodule instMin ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice ConvexCone.instCompleteLattice	—	—
toConvexCone_le_toConvexCone 📖	mathematical	—	ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder ConvexCone.instPartialOrder toConvexCone Submodule instPartialOrder	—	—
toConvexCone_top 📖	mathematical	—	toConvexCone Top.top Submodule instTop 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 ConvexCone.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	—

(root)

Definitions

Name	Category	Theorems
ConvexCone 📖	CompData	67 math math: ConvexCone.convex, Submodule.toConvexCone_inf, ConvexCone.mem_positive, ConvexCone.canLift, ConvexCone.coe_eq_empty, ConvexCone.coe_inf, ConvexCone.ext_iff, ConvexCone.coe_closure, ConvexCone.coe_zero, convexHull_toCone_eq_sInf, ConvexCone.coe_map, ConvexCone.coe_comap, Submodule.coe_toConvexCone, Submodule.toConvexCone_top, ConvexCone.notMem_bot, ConvexCone.isGenerating_bot, ConvexCone.mem_inf, ConvexCone.mem_iInf, ConvexCone.coe_strictlyPositive, ConvexCone.mem_map, ConvexCone.strictlyPositive_le_positive, ConvexCone.disjoint_hull_left_of_convex, ConvexCone.toPointedCone_top, ConvexCone.mem_top, ConvexCone.coe_mk, ConvexCone.subset_hull, ConvexCone.IsGenerating.top_le_span, ConvexCone.smul_mem_iff, Submodule.toConvexCone_le_toConvexCone, Convex.mem_toCone, ConvexCone.mem_add, ConvexCone.disjoint_coe, ConvexCone.pointed_zero, ConvexCone.instAddMemClass, ConvexCone.coe_positive, PointedCone.canLift, ConvexCone.mem_mk, Convex.toCone_isLeast, ConvexCone.mem_zero, ConvexCone.coe_add, convexHull_toCone_isLeast, ConvexCone.IsGenerating.span_eq_top, ConvexCone.disjoint_hull_right_of_convex, ConvexCone.isGenerating_top, Submodule.mem_toConvexCone, ConvexCone.hull_le_iff, ConvexCone.mem_strictlyPositive, ConvexCone.mem_hull_of_convex, ConvexCone.coe_iInf, ConvexCone.gc_hull_coe, ConvexCone.coe_top, PointedCone.mem_toConvexCone, ConvexCone.isGenerating_bot_iff, Convex.toCone_eq_sInf, ConvexCone.coe_hull_of_convex, Convex.subset_toCone, ConvexCone.closure_eq, ConvexCone.coe_sInf, Convex.mem_toCone', ConvexCone.mem_toPointedCone, ConvexCone.coe_bot, ConvexCone.IsReproducing.sub_eq_univ, Submodule.toConvexCone_bot, ConvexCone.mem_closure, PointedCone.toConvexCone_injective, ConvexCone.mem_sInf, ConvexCone.mem_comap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
convexHull_toCone_eq_sInf 📖	mathematical	—	Convex.toCone DFunLike.coe ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid convex_convexHull InfSet.sInf ConvexCone SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ConvexCone.instInfSet setOf Set.instHasSubset SetLike.coe ConvexCone.instSetLike	—	convex_convexHull IsGLB.sInf_eq IsLeast.isGLB convexHull_toCone_isLeast
convexHull_toCone_isLeast 📖	mathematical	—	IsLeast ConvexCone DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Preorder.toLE PartialOrder.toPreorder ConvexCone.instPartialOrder setOf Set Set.instHasSubset SetLike.coe ConvexCone.instSetLike Convex.toCone DFunLike.coe ClosureOperator OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike convexHull convex_convexHull	—	convex_convexHull Set.ext convexHull_min ConvexCone.convex HasSubset.Subset.trans Set.instIsTransSubset subset_convexHull Convex.toCone_isLeast

---

← Back to Index