Documentation Verification Report

DoubleDual

📁 Source: Mathlib/Analysis/Normed/Module/DoubleDual.lean

Statistics

Metric	Count
Definitions `inclusionInDoubleDual`, `inclusionInDoubleDualLi`, `inclusionInDoubleDualWeak`	3
Theorems `double_dual_bound`, `dual_def`, `inclusionInDoubleDualWeak_apply`, `inclusionInDoubleDualWeak_apply_apply`, `inclusionInDoubleDual_norm_eq`, `inclusionInDoubleDual_norm_le`, `isCompact_closure_of_isBounded`, `isEmbedding_inclusionInDoubleDualWeak`, `norm_le_dual_bound`, `toLinearMap_inclusionInDoubleDualWeak`	10
Total	13

NormedSpace

Definitions

Name	Category	Theorems
`inclusionInDoubleDual` 📖	CompOp	6 math math: `inclusionInDoubleDual_norm_eq`, `toLinearMap_inclusionInDoubleDualWeak`, `inclusionInDoubleDual_norm_le`, `inclusionInDoubleDualWeak_apply`, `double_dual_bound`, `dual_def`
`inclusionInDoubleDualLi` 📖	CompOp	—
`inclusionInDoubleDualWeak` 📖	CompOp	4 math math: `inclusionInDoubleDualWeak_apply_apply`, `toLinearMap_inclusionInDoubleDualWeak`, `inclusionInDoubleDualWeak_apply`, `isEmbedding_inclusionInDoubleDualWeak`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`double_dual_bound` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `ContinuousLinearMap.topologicalSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Semiring.toModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.hasOpNorm` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `DFunLike.coe` `ContinuousLinearMap` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousLinearMap.funLike` `inclusionInDoubleDual` `SeminormedAddCommGroup.toNorm`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `RingHomIsometric.ids` `one_mul` `ContinuousLinearMap.le_of_opNorm_le` `inclusionInDoubleDual_norm_le`
`dual_def` 📖	mathematical	—	`DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `ContinuousLinearMap.topologicalSpace` `RingHom.id` `Semiring.toNonAssocSemiring` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Semiring.toModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.funLike` `ContinuousLinearMap` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `inclusionInDoubleDual`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul`
`inclusionInDoubleDualWeak_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `WeakSpace` `Semifield.toCommSemiring` `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` `CommSemiring.toSemiring` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `SeminormedAddCommGroup.toPseudoMetricSpace` `instTopologicalSpaceWeakSpace` `instAddCommMonoidWeakSpace` `WeakDual` `StrongDual` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `ContinuousLinearMap.module` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Algebra.id` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instTopologicalSpaceWeakDual` `instAddCommMonoidWeakDual` `WeakSpace.instModule'` `WeakDual.instModule'` `ContinuousLinearMap.funLike` `inclusionInDoubleDualWeak` `LinearEquiv` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `StrongDual.toWeakDual` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `inclusionInDoubleDual` `LinearEquiv.symm` `toWeakSpace`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Algebra.to_smulCommClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`inclusionInDoubleDualWeak_apply_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Semiring.toModule` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `ContinuousLinearMap.module` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `ContinuousLinearMap.funLike` `WeakSpace` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `instTopologicalSpaceWeakSpace` `instAddCommMonoidWeakSpace` `WeakDual` `Algebra.to_smulCommClass` `Algebra.id` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instTopologicalSpaceWeakDual` `instAddCommMonoidWeakDual` `WeakSpace.instModule'` `WeakDual.instModule'` `inclusionInDoubleDualWeak` `LinearEquiv` `EquivLike.toFunLike` `LinearEquiv.instEquivLike` `LinearEquiv.symm` `toWeakSpace`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Algebra.to_smulCommClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`inclusionInDoubleDual_norm_eq` 📖	mathematical	—	`Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `StrongDual` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `toModule` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Semiring.toModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousLinearMap.hasOpNorm` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `inclusionInDoubleDual` `ContinuousLinearMap.id`	—	`ContinuousLinearMap.opNorm_flip` `Algebra.to_smulCommClass` `RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`inclusionInDoubleDual_norm_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `StrongDual` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `toModule` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `Semiring.toModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `IsSemitopologicalSemiring.toContinuousAdd` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `ContinuousLinearMap.module` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousLinearMap.hasOpNorm` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `inclusionInDoubleDual` `Real.instOne`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `RingHomIsometric.ids` `inclusionInDoubleDual_norm_eq` `ContinuousLinearMap.norm_id_le`
`isCompact_closure_of_isBounded` 📖	mathematical	`Bornology.IsBounded` `PseudoMetricSpace.toBornology` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.preimage` `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` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `toModule` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `instAddCommMonoidWeakSpace` `WeakSpace.instModule'` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toWeakSpace` `Set` `WeakDual` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `ContinuousLinearMap.module` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Algebra.id` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Set.instHasSubset` `closure` `instTopologicalSpaceWeakDual` `Set.image` `ContinuousLinearMap` `instTopologicalSpaceWeakSpace` `instAddCommMonoidWeakDual` `WeakDual.instModule'` `ContinuousLinearMap.funLike` `inclusionInDoubleDualWeak` `Set.range`	`IsCompact` `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` `ESeminormedAddCommMonoid.toAddCommMonoid` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `toModule` `instTopologicalSpaceWeakSpace` `closure`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `RingHomInvPair.ids` `Algebra.to_smulCommClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Topology.IsEmbedding.closure_eq_preimage_closure_image` `isEmbedding_inclusionInDoubleDualWeak` `Topology.IsInducing.isCompact_preimage'` `Topology.IsEmbedding.toIsInducing` `WeakDual.isCompact_of_bounded_of_closed` `RingHomIsometric.ids` `FiniteDimensional.proper_real` `FiniteDimensional.rclike_to_real` `WeakDual.isBounded_closure` `LipschitzWith.isBounded_image` `ContinuousLinearMap.lipschitz` `isClosed_closure`
`isEmbedding_inclusionInDoubleDualWeak` 📖	mathematical	—	`Topology.IsEmbedding` `WeakSpace` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `DenselyNormedField.toNontriviallyNormedField` `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` `SeminormedAddCommGroup.toAddCommGroup` `NormedAddCommGroup.toSeminormedAddCommGroup` `toModule` `SeminormedAddCommGroup.toPseudoMetricSpace` `WeakDual` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `ContinuousLinearMap.addCommMonoid` `RingHom.id` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `ContinuousLinearMap.module` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Algebra.id` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instTopologicalSpaceWeakSpace` `instTopologicalSpaceWeakDual` `DFunLike.coe` `ContinuousLinearMap` `instAddCommMonoidWeakSpace` `instAddCommMonoidWeakDual` `WeakSpace.instModule'` `WeakDual.instModule'` `ContinuousLinearMap.funLike` `inclusionInDoubleDualWeak`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Algebra.to_smulCommClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `induced_compose` `RingHomInvPair.ids` `LinearEquiv.injective` `LinearIsometry.injective` `RingHomIsometric.ids`
`norm_le_dual_bound` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Norm.norm` `NormedField.toNorm` `DenselyNormedField.toNormedField` `RCLike.toDenselyNormedField` `DFunLike.coe` `StrongDual` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `ContinuousLinearMap.funLike` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule` `Real.instMul` `ContinuousLinearMap.hasOpNorm` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `DenselyNormedField.toNontriviallyNormedField` `NormedField.toNormedSpace` `NontriviallyNormedField.toNormedField`	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Algebra.to_smulCommClass` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `RingHomIsometric.ids` `LinearIsometry.norm_map` `ContinuousLinearMap.opNorm_le_bound`
`toLinearMap_inclusionInDoubleDualWeak` 📖	mathematical	—	`ContinuousLinearMap.toLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `WeakSpace` `Semifield.toCommSemiring` `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` `CommSemiring.toSemiring` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `toModule` `SeminormedAddCommGroup.toPseudoMetricSpace` `instTopologicalSpaceWeakSpace` `instAddCommMonoidWeakSpace` `WeakDual` `StrongDual` `ContinuousLinearMap.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Semiring.toModule` `ContinuousLinearMap.module` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `Algebra.to_smulCommClass` `Algebra.id` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `instTopologicalSpaceWeakDual` `instAddCommMonoidWeakDual` `WeakSpace.instModule'` `WeakDual.instModule'` `inclusionInDoubleDualWeak` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `LinearMap` `LinearMap.addCommMonoid` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `LinearEquiv.arrowCongr` `RingHomCompTriple.ids` `toWeakSpace` `StrongDual.toWeakDual` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `inclusionInDoubleDual`	—	`IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeparatelyContinuousMul.to_continuousSMul` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `Algebra.to_smulCommClass` `SeminormedAddCommGroup.toIsTopologicalAddGroup`

---

← Back to Index