Dual

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

Statistics

Metric	Count
Definitions dual	1
Theorems dual_dual_flip_dual, dual_empty, dual_eq_iInter_dual_singleton, dual_flip_dual_dual_flip, dual_iUnion, dual_insert, dual_le_dual, dual_sUnion, dual_singleton, dual_span, dual_union, dual_univ, dual_zero, mem_dual, subset_dual_dual	15
Total	16

PointedCone

Definitions

Name	Category	Theorems
dual 📖	CompOp	17 math math: subset_dual_dual, dual_union, mem_dual, dual_empty, dual_insert, dual_zero, dual_iUnion, dual_le_dual, isClosed_dual, dual_flip_dual_dual_flip, dual_sUnion, ProperCone.innerDual_toSubmodule, dual_univ, dual_eq_iInter_dual_singleton, dual_dual_flip_dual, dual_singleton, dual_span

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dual_dual_flip_dual 📖	mathematical	—	dual SetLike.coe PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule LinearMap.flip NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id	—	Algebra.to_smulCommClass le_antisymm IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono dual_le_dual subset_dual_dual
dual_empty 📖	mathematical	—	dual Set Set.instEmptyCollection Top.top PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instTop Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass ext IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono instIsEmptyFalse
dual_eq_iInter_dual_singleton 📖	mathematical	—	SetLike.coe PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule dual Set.iInter Set.Elem Set Set.instSingletonSet Set.instMembership	—	Algebra.to_smulCommClass Set.ext IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Set.iInter_coe_set Set.iInter_congr_Prop
dual_flip_dual_dual_flip 📖	mathematical	—	dual LinearMap.flip CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass dual_dual_flip_dual
dual_iUnion 📖	mathematical	—	dual Set.iUnion iInf PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass ext IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono forall_swap
dual_insert 📖	mathematical	—	dual Set Set.instInsert PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instMin Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule Set.instSingletonSet	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Set.insert_eq dual_union
dual_le_dual 📖	mathematical	Set Set.instHasSubset	PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule dual	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
dual_sUnion 📖	mathematical	—	dual Set.sUnion InfSet.sInf PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instInfSet Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule Set.image Set	—	Algebra.to_smulCommClass ext IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono forall_swap
dual_singleton 📖	mathematical	—	dual Set Set.instSingletonSet comap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.instFunLike positive IsOrderedRing.toIsOrderedAddMonoid IsOrderedModule.toPosSMulMono SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring IsOrderedRing.toIsOrderedModule	—	Algebra.to_smulCommClass ext IsOrderedRing.toIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsOrderedRing.toIsOrderedModule IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
dual_span 📖	mathematical	—	dual SetLike.coe PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule span	—	Algebra.to_smulCommClass le_antisymm IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono dual_le_dual Submodule.subset_span Submodule.span_induction map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass LinearMap.add_apply add_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul Nonneg.instIsScalarTower IsScalarTower.left LinearMap.instIsScalarTower IsScalarTower.right Nonneg.mk_smul LinearMap.smul_apply mul_nonneg
dual_union 📖	mathematical	—	dual Set Set.instUnion PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instMin Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass ext IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
dual_univ 📖	mathematical	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule DFunLike.coe LinearMap.addCommMonoid LinearMap.module SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id LinearMap.instFunLike LinearMap.flip	dual Set.univ PointedCone Submodule.pointwiseZero Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass SMulCommClass.symm le_antisymm IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono map_eq_zero_iff AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass LinearMap.ext LE.le.antisymm' Set.mem_univ map_neg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
dual_zero 📖	mathematical	—	dual Set Set.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Top.top PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.instTop Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass ext IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
mem_dual 📖	mathematical	—	PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule dual NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
subset_dual_dual 📖	mathematical	—	Set Set.instHasSubset SetLike.coe PointedCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule dual LinearMap.flip NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono

---

← Back to Index