Basic

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

Statistics

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

ConvexCone

Theorems

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

ConvexCone.Pointed

Theorems

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

ProperCone

Definitions

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

Theorems

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

(root)

Definitions

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

---

← Back to Index