WeakSpace

📁 Source: Mathlib/Analysis/LocallyConvex/WeakSpace.lean

Statistics

Metric	Count
Definitions WeakSpace	1
Theorems toWeakSpace_closure, image_closure_of_convex, image_closure_of_convex', image_closure_of_convex, toWeakSpace_closedConvexHull_eq	5
Total	6

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toWeakSpace_closure 📖	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	Set.image WeakSpace Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Algebra.toSMul Algebra.id Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids instAddCommMonoidWeakSpace WeakSpace.instModule' EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toWeakSpace closure instTopologicalSpaceWeakSpace	—	le_antisymm IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul RingHomInvPair.ids ContinuousOn.image_closure Continuous.continuousOn ContinuousMapClass.map_continuous ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass Set.compl_subset_compl Eq.subset Set.instReflSubset Equiv.image_compl IsScalarTower.continuousSMul IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul RCLike.geometric_hahn_banach_closed_point closure ContinuousSMul.continuousConstSMul isClosed_closure EquivLike.toEmbeddingLike RingHomCompTriple.ids WeakBilin.eval_continuous Algebra.to_smulCommClass LinearMap.IsScalarTower.compatibleSMul WeakSpace.instIsScalarTower IsScalarTower.right LinearEquiv.symm_apply_apply closure_minimal LT.lt.le subset_closure isClosed_le OrderTopology.to_orderClosedTopology instOrderTopologyReal ContinuousLinearMap.continuous continuous_const LT.lt.not_ge

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_closure_of_convex 📖	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 Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe Module.Dual CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField LinearMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearEquiv RingHomInvPair.ids LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv dualMap ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring symm	Set.image closure	—	RingHomInvPair.ids smulCommClass_self le_antisymm LinearMap.image_closure_of_convex Set.image_subset_image_iff injective Set.image_image Set.image_congr symm_apply_apply Set.image_id' LinearMap.IsScalarTower.compatibleSMul Convex.linear_image
image_closure_of_convex' 📖	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 ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule DFunLike.coe Equiv StrongDual EquivLike.toFunLike Equiv.instEquivLike LinearEquiv CommSemiring.toSemiring Semifield.toCommSemiring RingHomInvPair.ids Module.Dual LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid DFinsupp.instEquivLikeLinearEquiv dualMap	Set.image closure	—	RingHomInvPair.ids smulCommClass_self Equiv.apply_symm_apply dualMap_apply ContinuousLinearMap.coe_coe apply_symm_apply image_closure_of_convex ContinuousMapClass.map_continuous ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_closure_of_convex 📖	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 Continuous UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField DFunLike.coe Module.Dual CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield NormedField.toField instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule RingHom.id LinearMap addCommMonoid module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid dualMap ContinuousLinearMap.toLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring	Set Set.instHasSubset Set.image closure	—	smulCommClass_self IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul RingHomInvPair.ids WeakBilin.continuous_of_continuous_eval WeakBilin.eval_continuous Convex.linear_image IsScalarTower.compatibleSMul Set.image_subset_image_iff LinearEquiv.injective Convex.toWeakSpace_closure Set.image_image Set.image_congr LinearEquiv.symm_apply_apply ContinuousOn.image_closure Continuous.continuousOn

(root)

Definitions

Name	Category	Theorems
WeakSpace 📖	CompOp	10 math math: WeakSpace.map_apply, toWeakSpaceCLM_bijective, WeakSpace.instIsTopologicalAddGroup, isOpenMap_toWeakSpace_symm, Convex.toWeakSpace_closure, toWeakSpace_closedConvexHull_eq, WeakSpace.instContinuousSMul, WeakSpace.coe_map, toWeakSpaceCLM_eq_toWeakSpace, WeakSpace.instIsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toWeakSpace_closedConvexHull_eq 📖	mathematical	—	Set.image WeakSpace Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing IsTopologicalSemiring.toContinuousAdd NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Algebra.toSMul Algebra.id Ring.uniformContinuousConstSMul NormedRing.toRing NormedCommRing.toNormedRing SeminormedAddCommGroup.to_isUniformAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing IsTopologicalSemiring.toContinuousMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddCommGroup.toAddCommMonoid DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids instAddCommMonoidWeakSpace WeakSpace.instModule' EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toWeakSpace ClosureOperator Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike closedConvexHull DivisionSemiring.toSemiring Semifield.toDivisionSemiring RCLike.toPartialOrder WeakSpace.instAddCommGroup EuclideanDomain.toCommRing Field.toEuclideanDomain SeminormedAddCommGroup.toIsTopologicalAddGroup instTopologicalSpaceWeakSpace	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup closedConvexHull_eq_closure_convexHull ContinuousSMul.continuousConstSMul Convex.toWeakSpace_closure Convex.lift RCLike.toZeroLEOneClass PosSMulMono.toSMulPosMono Real.instIsOrderedRing RCLike.toIsOrderedAddMonoid IsOrderedModule.toPosSMulMono instIsOrderedModule RCLike.toStarOrderedRing RCLike.instStarModuleReal IsScalarTower.right Algebra.to_smulCommClass convex_convexHull WeakSpace.instIsTopologicalAddGroup WeakSpace.instContinuousSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology LinearMap.image_convexHull

---

← Back to Index