Dual

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

Statistics

Metric	Count
Definitions dual	1
Theorems isClosed_dual, dual_dual_flip, dual_empty, dual_flip_dual, dual_iUnion, dual_insert, dual_le_dual, dual_sUnion, dual_singleton, dual_union, dual_univ, dual_zero, hyperplane_separation, hyperplane_separation_point, mem_dual, subset_dual_dual	16
Total	17

PointedCone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isClosed_dual 📖	mathematical	Continuous DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id	IsClosed SetLike.coe PointedCone Submodule.setLike Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule dual	—	Algebra.to_smulCommClass IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Set.biUnion_of_singleton dual_iUnion Submodule.coe_iInf IsOrderedRing.toIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsOrderedRing.toIsOrderedModule Set.iInter_congr_Prop dual_singleton isClosed_biInter IsClosed.preimage isClosed_Ici

ProperCone

Definitions

Name	Category	Theorems
dual 📖	CompOp	13 math math: dual_insert, dual_sUnion, mem_dual, subset_dual_dual, dual_univ, dual_iUnion, dual_singleton, dual_zero, dual_flip_dual, dual_dual_flip, dual_empty, dual_le_dual, dual_union

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dual_dual_flip 📖	mathematical	—	dual Real Real.commRing Real.partialOrder Real.instIsOrderedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instClosedIciTopology PartialOrder.toPreorder OrderTopology.to_orderClosedTopology Real.linearOrder instOrderTopologyReal SetLike.coe ProperCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instSetLike LinearMap.flip Real.semiring Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Algebra.to_smulCommClass Real.instCommSemiring Algebra.id RingHom.id Semiring.toNonAssocSemiring LinearMap.flip.instIsContPerfPair	—	Algebra.to_smulCommClass Real.instIsOrderedRing dual_flip_dual LinearMap.flip.instIsContPerfPair
dual_empty 📖	mathematical	—	dual Set Set.instEmptyCollection Top.top ProperCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid OrderTop.toTop Preorder.toLE ClosedSubmodule PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule ClosedSubmodule.instPartialOrder ClosedSubmodule.instOrderTop	—	Algebra.to_smulCommClass ext IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono instIsEmptyFalse
dual_flip_dual 📖	mathematical	—	dual Real Real.commRing Real.partialOrder Real.instIsOrderedRing UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace instClosedIciTopology PartialOrder.toPreorder OrderTopology.to_orderClosedTopology Real.linearOrder instOrderTopologyReal LinearMap.flip Real.semiring AddCommGroup.toAddCommMonoid Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing NormedField.toNormedSpace Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id RingHom.id Semiring.toNonAssocSemiring LinearMap.flip.instIsContPerfPair SetLike.coe ProperCone CommRing.toCommSemiring instSetLike	—	Algebra.to_smulCommClass Real.instIsOrderedRing le_antisymm instClosedIciTopology OrderTopology.to_orderClosedTopology instOrderTopologyReal LinearMap.flip.instIsContPerfPair Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_forall_eq RingHomInvPair.ids IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul Function.Surjective.exists LinearEquiv.surjective hyperplane_separation_point subset_dual_dual
dual_iUnion 📖	mathematical	—	dual Set.iUnion iInf ProperCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ClosedSubmodule.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 ProperCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ClosedSubmodule.instInf 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	ProperCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder dual	—	Algebra.to_smulCommClass
dual_sUnion 📖	mathematical	—	dual Set.sUnion InfSet.sInf ProperCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ClosedSubmodule.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 NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids StrongDual ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsTopologicalRing.toIsTopologicalSemiring ContinuousLinearMap.module Algebra.to_smulCommClass Algebra.id SMulCommClass.continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toContPerfPair positive IsOrderedRing.toIsOrderedAddMonoid IsOrderedModule.toPosSMulMono PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass IsOrderedRing.toIsOrderedModule	—	Algebra.to_smulCommClass ext RingHomInvPair.ids IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul IsOrderedRing.toIsOrderedAddMonoid IsOrderedModule.toPosSMulMono IsOrderedRing.toIsOrderedModule IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono
dual_union 📖	mathematical	—	dual Set Set.instUnion ProperCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ClosedSubmodule.instInf 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	—	dual Set.univ Bot.bot ProperCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid 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	—	Algebra.to_smulCommClass le_antisymm IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono RingHomInvPair.ids IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring SMulCommClass.continuousConstSMul IsTopologicalSemiring.toContinuousMul LinearMap.flip.instIsContPerfPair map_eq_zero_iff AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass LinearEquiv.injective ContinuousLinearMap.ext LE.le.antisymm' Set.mem_univ map_neg LinearMap.semilinearMapClass IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid
dual_zero 📖	mathematical	—	dual Set Set.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Top.top ProperCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid OrderTop.toTop Preorder.toLE ClosedSubmodule PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Nonneg.semiring IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono Nonneg.instModule ClosedSubmodule.instPartialOrder ClosedSubmodule.instOrderTop	—	Algebra.to_smulCommClass ext IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
hyperplane_separation 📖	mathematical	Convex Real Real.semiring Real.partialOrder AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction IsCompact Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe ProperCone Real.instIsOrderedRing instSetLike	Real.instLE Real.instZero DFunLike.coe StrongDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instLT	—	Real.instIsOrderedRing Set.eq_empty_or_nonempty geometric_hahn_banach_compact_closed convex isClosed map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Submodule.zero_mem IsOrderedRing.toZeroLEOneClass IsOrderedRing.toPosMulMono map_smul SemilinearMapClass.toMulActionSemiHomClass inv_mul_cancel_right₀ LT.lt.ne smul_mem le_of_lt mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le inv_neg'' LT.lt.trans_le LE.le.trans LT.lt.le
hyperplane_separation_point 📖	mathematical	ProperCone Real Real.semiring Real.partialOrder Real.instIsOrderedRing AddCommGroup.toAddCommMonoid SetLike.instMembership instSetLike	Real.instLE Real.instZero DFunLike.coe StrongDual UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ContinuousLinearMap.funLike RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Real.instLT	—	Real.instIsOrderedRing hyperplane_separation convex_singleton
mem_dual 📖	mathematical	—	ProperCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership instSetLike dual Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid Semiring.toModule LinearMap.instFunLike LinearMap.addCommMonoid LinearMap.module Algebra.to_smulCommClass Algebra.id	—	Algebra.to_smulCommClass
subset_dual_dual 📖	mathematical	—	Set Set.instHasSubset SetLike.coe ProperCone CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instSetLike dual LinearMap.flip NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.to_smulCommClass Algebra.id RingHom.id Semiring.toNonAssocSemiring LinearMap.flip.instIsContPerfPair	—	Algebra.to_smulCommClass

---

← Back to Index