Dual

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

Statistics

Metric	Count
Definitions dual	1
Theorems dual_anti, dual_antitone, dual_dual_flip_dual, dual_empty, dual_eq_comap_dual_eval, dual_eq_dual_id_image, dual_eq_dual_id_map, dual_eq_iInter_dual_singleton, dual_flip_dual_dual_flip, dual_hull, dual_iUnion, dual_image, dual_insert, dual_ker, dual_le_dual, dual_neg, dual_sUnion, dual_singleton, dual_singleton_zero, dual_span, dual_sup, dual_union, dual_univ, dual_zero, mem_dual, subset_dual_dual, subset_dual_flip_iff_subset_dual	27
Total	28

PointedCone

Definitions

Name	Category	Theorems
dual 📖	CompOp	38 math math: dual_sup, DualFG.dual_dual_flip, dual_hull, subset_dual_dual, dual_ker, DualFG.exists_fg_dual, dual_union, mem_dual, DualFG.dual_flip_dual, dual_empty, FG.dual_dualfg, dual_insert, dual_antitone, basis_coord_mem_dual, dual_zero, dual_iUnion, DualFG.dual_of_finset, dual_le_dual, subset_dual_flip_iff_subset_dual, DualFG.dual_of_fg, isClosed_dual, dual_eq_comap_dual_eval, DualFG.dual_of_finite, dual_singleton_zero, dual_neg, dual_flip_dual_dual_flip, dual_sUnion, ProperCone.innerDual_toSubmodule, dual_image, dual_anti, DualFG.iff_exists_fg_dual, dual_univ, dual_eq_iInter_dual_singleton, dual_dual_flip_dual, dual_eq_dual_id_map, dual_singleton, dual_eq_dual_id_image, dual_span

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dual_anti 📖	mathematical	Set Set.instHasSubset	PointedCone CommSemiring.toSemiring 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_antitone 📖	mathematical	—	Antitone Set PointedCone CommSemiring.toSemiring PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Submodule.instPartialOrder Preorder.toLE MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule dual	—	Algebra.to_smulCommClass dual_anti
dual_dual_flip_dual 📖	mathematical	—	dual SetLike.coe PointedCone CommSemiring.toSemiring 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 Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id	—	Algebra.to_smulCommClass le_antisymm IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono dual_anti subset_dual_dual
dual_empty 📖	mathematical	—	dual Set Set.instEmptyCollection Top.top PointedCone CommSemiring.toSemiring 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_comap_dual_eval 📖	mathematical	—	dual comap LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule 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.flip Module.Dual.eval	—	Algebra.to_smulCommClass ext SMulCommClass.symm IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
dual_eq_dual_id_image 📖	mathematical	—	dual LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.id Set.image DFunLike.coe LinearMap.instFunLike	—	Algebra.to_smulCommClass dual_image
dual_eq_dual_id_map 📖	mathematical	—	dual SetLike.coe PointedCone CommSemiring.toSemiring Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id LinearMap.id map	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono dual_image
dual_eq_iInter_dual_singleton 📖	mathematical	—	SetLike.coe PointedCone CommSemiring.toSemiring 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 NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass dual_dual_flip_dual
dual_hull 📖	mathematical	—	dual SetLike.coe PointedCone CommSemiring.toSemiring Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule hull	—	Algebra.to_smulCommClass le_antisymm IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono dual_anti Submodule.subset_span Submodule.span_induction map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass instReflLe 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_iUnion 📖	mathematical	—	dual Set.iUnion iInf PointedCone CommSemiring.toSemiring 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
dual_image 📖	mathematical	—	dual Set.image DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.comp NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id RingHomCompTriple.ids	—	Algebra.to_smulCommClass ext RingHomCompTriple.ids IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
dual_insert 📖	mathematical	—	dual Set Set.instInsert PointedCone CommSemiring.toSemiring 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_ker 📖	mathematical	—	dual SetLike.coe Submodule CommSemiring.toSemiring Submodule.setLike LinearMap.ker LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id Top.top PointedCone Submodule.instTop Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule	—	Algebra.to_smulCommClass ext IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono instReflLe
dual_le_dual 📖	mathematical	Set Set.instHasSubset	PointedCone CommSemiring.toSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule dual	—	dual_anti
dual_neg 📖	mathematical	—	dual CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid PointedCone CommSemiring.toSemiring Submodule.pointwiseNeg 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_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
dual_sUnion 📖	mathematical	—	dual Set.sUnion InfSet.sInf PointedCone CommSemiring.toSemiring 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
dual_singleton 📖	mathematical	—	dual Set Set.instSingletonSet comap CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id 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 IsOrderedRing.toIsOrderedModule	—	Algebra.to_smulCommClass ext IsOrderedRing.toIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsOrderedRing.toIsOrderedModule IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
dual_singleton_zero 📖	mathematical	—	dual Set Set.instSingletonSet AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Top.top PointedCone CommSemiring.toSemiring 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 dual_zero
dual_span 📖	mathematical	—	dual SetLike.coe PointedCone CommSemiring.toSemiring Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule hull	—	dual_hull
dual_sup 📖	mathematical	—	dual SetLike.coe PointedCone CommSemiring.toSemiring Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Set Set.instUnion	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsScalarTower.left Submodule.span_coe_eq_restrictScalars Submodule.restrictScalars_self Submodule.span_union
dual_union 📖	mathematical	—	dual Set Set.instUnion PointedCone CommSemiring.toSemiring 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 CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set.univ PointedCone CommSemiring.toSemiring Submodule.pointwiseZero Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring 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 AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Top.top PointedCone CommSemiring.toSemiring 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 instReflLe
mem_dual 📖	mathematical	—	PointedCone CommSemiring.toSemiring 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 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 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 Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
subset_dual_flip_iff_subset_dual 📖	mathematical	—	Set Set.instHasSubset SetLike.coe PointedCone CommSemiring.toSemiring 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 Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono le_trans subset_dual_dual dual_antitone

---

← Back to Index