Pointed

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

Statistics

Metric	Count
Definitions `Pointed`, `toPointedCone`, `Pointed`, `PointedCone`, `comap`, `instCoeConvexCone`, `instZero`, `map`, `ofConeComb`, `positive`, `span`, `toConvexCone`, `Pointed`	13
Theorems `coe_toPointedCone`, `mem_toPointedCone`, `toPointedCone_top`, `canLift`, `coe_comap`, `coe_map`, `comap_comap`, `comap_id`, `convex`, `ext`, `ext_iff`, `map_id`, `map_map`, `mem_comap`, `mem_map`, `mem_positive`, `mem_span_set`, `mem_toConvexCone`, `pointed_toConvexCone`, `salient_iff_inter_neg_eq_singleton`, `smul_mem`, `subset_span`, `toConvexCone_injective`, `toConvexCone_map`, `toConvexCone_positive`, `to_isOrderedModule`	26
Total	39

ConvexCone

Definitions

Name	Category	Theorems
`Pointed` 📖	MathDef	11 math math: `PointedCone.toConvexCone_closure_pointed`, `pointed_positive`, `PointedCone.pointed_toConvexCone`, `Flat.pointed`, `pointed_iff_not_blunt`, `pointed_zero`, `Submodule.pointed_toConvexCone`, `PointedCone.canLift`, `ProperCone.pointed_toConvexCone`, `Pointed.of_nonempty_of_isClosed`, `blunt_iff_not_pointed`
`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` `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	5 math math: `comap_comap`, `comap_id`, `mem_comap`, `coe_comap`, `dual_singleton`
`instCoeConvexCone` 📖	CompOp	—
`instZero` 📖	CompOp	—
`map` 📖	CompOp	9 math math: `map_id`, `ProperCone.mem_map`, `coe_map`, `map_map`, `mem_map`, `ProperCone.coe_map`, `minTensorProduct_comm`, `maxTensorProduct_comm`, `toConvexCone_map`
`ofConeComb` 📖	CompOp	—
`positive` 📖	CompOp	4 math math: `ProperCone.toPointedCone_positive`, `mem_positive`, `toConvexCone_positive`, `dual_singleton`
`span` 📖	CompOp	4 math math: `subset_span`, `mem_span_set`, `IsSimplicial.span`, `dual_span`
`toConvexCone` 📖	CompOp	11 math math: `toConvexCone_closure_pointed`, `ConvexCone.canLift`, `ConvexCone.coe_toPointedCone`, `pointed_toConvexCone`, `canLift`, `toConvexCone_map`, `ProperCone.pointed_toConvexCone`, `mem_toConvexCone`, `toConvexCone_positive`, `salient_iff_inter_neg_eq_singleton`, `toConvexCone_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`canLift` 📖	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`	—	—
`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_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`
`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`
`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_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_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` `span` `Set` `Set.instHasSubset` `SetLike.coe` `Finset` `Finset.instSetLike` `Finsupp.support` `DFunLike.coe` `Finsupp` `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_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`	—	—
`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`	`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_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` `span`	—	`Submodule.subset_span` `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` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `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	41 math math: `ProperCone.mem_map`, `PointedCone.coe_map`, `PointedCone.subset_dual_dual`, `PointedCone.dual_union`, `PointedCone.mem_dual`, `PointedCone.dual_empty`, `PointedCone.dual_insert`, `ConvexCone.toPointedCone_top`, `PointedCone.convex`, `PointedCone.mem_map`, `PointedCone.coe_closure`, `PointedCone.tmul_subset_maxTensorProduct`, `PointedCone.dual_zero`, `PointedCone.minTensorProduct_le_maxTensorProduct`, `PointedCone.tmul_subset_minTensorProduct`, `PointedCone.subset_span`, `PointedCone.ext_iff`, `PointedCone.dual_iUnion`, `PointedCone.mem_span_set`, `ProperCone.toPointedCone_bot`, `PointedCone.canLift`, `PointedCone.dual_le_dual`, `ProperCone.toPointedCone_injective`, `PointedCone.mem_closure`, `PointedCone.mem_comap`, `PointedCone.mem_toConvexCone`, `PointedCone.isClosed_dual`, `PointedCone.mem_positive`, `PointedCone.mem_maxTensorProduct`, `PointedCone.dual_flip_dual_dual_flip`, `ProperCone.mem_toPointedCone`, `PointedCone.dual_sUnion`, `ConvexCone.mem_toPointedCone`, `PointedCone.closure_eq`, `PointedCone.dual_univ`, `PointedCone.dual_eq_iInter_dual_singleton`, `PointedCone.dual_dual_flip_dual`, `PointedCone.coe_comap`, `PointedCone.salient_iff_inter_neg_eq_singleton`, `PointedCone.toConvexCone_injective`, `PointedCone.dual_span`

---

← Back to Index