Documentation Verification Report

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`, `instT2SpaceWeakSpaceOfSeparatingDual`, `toWeakSpace_closedConvexHull_eq`	6
Total	7

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` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `AddCommGroup.toAddCommMonoid` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `instAddCommMonoidWeakSpace` `WeakSpace.instModule'` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toWeakSpace` `closure` `instTopologicalSpaceWeakSpace`	—	`le_antisymm` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `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` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `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` `DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `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` `DFunLike.coe` `LinearEquiv` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `AddCommGroup.toAddCommMonoid` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `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` `DFunLike.coe` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike` `closure`	—	`smulCommClass_self` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `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	16 math math: `WeakSpace.map_apply`, `toWeakSpaceCLM_bijective`, `WeakSpace.instIsTopologicalAddGroup`, `instT2SpaceWeakSpaceOfSeparatingDual`, `NormedSpace.inclusionInDoubleDualWeak_apply_apply`, `isOpenMap_toWeakSpace_symm`, `NormedSpace.toLinearMap_inclusionInDoubleDualWeak`, `Convex.toWeakSpace_closure`, `NormedSpace.inclusionInDoubleDualWeak_apply`, `toWeakSpace_closedConvexHull_eq`, `NormedSpace.isCompact_closure_of_isBounded`, `NormedSpace.isEmbedding_inclusionInDoubleDualWeak`, `WeakSpace.instContinuousSMul`, `WeakSpace.coe_map`, `toWeakSpaceCLM_eq_toWeakSpace`, `WeakSpace.instIsScalarTower`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instT2SpaceWeakSpaceOfSeparatingDual` 📖	mathematical	—	`T2Space` `WeakSpace` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instTopologicalSpaceWeakSpace`	—	`Topology.IsEmbedding.t2Space` `Algebra.to_smulCommClass` `Pi.t2Space` `WeakBilin.isEmbedding` `SeparatingDual.exists_separating_of_ne` `DFunLike.congr_fun`
`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` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `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` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `instTopologicalSpaceWeakSpace`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `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` `IsTopologicalRing.toIsTopologicalSemiring` `LinearMap.image_convexHull`

---

← Back to Index