Documentation Verification Report

Closure

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

Statistics

Metric	Count
Definitions `closure`, `closure`	2
Theorems `closure_eq`, `coe_closure`, `mem_closure`, `closure_eq`, `coe_closure`, `mem_closure`, `toConvexCone_closure_pointed`	7
Total	9

ConvexCone

Definitions

Name	Category	Theorems
`closure` 📖	CompOp	4 math math: `PointedCone.toConvexCone_closure_pointed`, `coe_closure`, `closure_eq`, `mem_closure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq` 📖	mathematical	—	`closure` `closure` `SetLike.coe` `ConvexCone` `instSetLike`	—	`SetLike.ext'_iff`
`coe_closure` 📖	mathematical	—	`SetLike.coe` `ConvexCone` `instSetLike` `closure` `closure`	—	—
`mem_closure` 📖	mathematical	—	`ConvexCone` `SetLike.instMembership` `instSetLike` `closure` `Set` `Set.instMembership` `closure` `SetLike.coe`	—	—

PointedCone

Definitions

Name	Category	Theorems
`closure` 📖	CompOp	5 math math: `ProperCone.mem_map`, `coe_closure`, `ProperCone.coe_map`, `mem_closure`, `closure_eq`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq` 📖	mathematical	—	`closure` `closure` `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`	—	`SetLike.ext'_iff` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono`
`coe_closure` 📖	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` `closure` `closure`	—	`IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono`
`mem_closure` 📖	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` `closure` `Set` `Set.instMembership` `closure` `SetLike.coe`	—	`IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono`
`toConvexCone_closure_pointed` 📖	mathematical	—	`ConvexCone.Pointed` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `ConvexCone.closure` `toConvexCone`	—	`subset_closure` `pointed_toConvexCone`

---

← Back to Index