Documentation Verification Report

ContinuousLinearMap

📁 Source: Mathlib/Analysis/Normed/Operator/ContinuousLinearMap.lean

Statistics

Metric	Count
Definitions `ofHomothety`, `ofHomothety`, `toContinuousLinearEquivOfBounds`, `mkContinuous`, `mkContinuousOfExistsBound`, `toContinuousLinearMap₁`	6
Theorems `homothety_inverse`, `antilipschitz_of_bound`, `bound_of_antilipschitz`, `isUniformEmbedding_of_bound`, `mkContinuousOfExistsBound_apply`, `mkContinuousOfExistsBound_coe`, `mkContinuous_apply`, `mkContinuous_coe`, `toContinuousLinearMap₁_apply`, `toContinuousLinearMap₁_coe`, `continuous_of_linear_of_bound`, `continuous_of_linear_of_boundₛₗ`	12
Total	18

ContinuousLinearEquiv

Definitions

Name	Category	Theorems
`ofHomothety` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`homothety_inverse` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `LinearEquiv` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Real.instMul`	`LinearEquiv.symm` `Real.instInv`	—	`mul_assoc` `inv_mul_cancel₀` `ne_of_lt` `one_mul` `LinearEquiv.apply_symm_apply`

ContinuousLinearMap

Definitions

Name	Category	Theorems
`ofHomothety` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antilipschitz_of_bound` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul` `NNReal.toReal` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `funLike`	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace`	—	`AddMonoidHomClass.antilipschitz_of_bound` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `continuousSemilinearMapClass`
`bound_of_antilipschitz` 📖	mathematical	`AntilipschitzWith` `PseudoMetricSpace.toPseudoEMetricSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `funLike`	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul` `NNReal.toReal`	—	`ZeroHomClass.bound_of_antilipschitz` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `continuousSemilinearMapClass`
`isUniformEmbedding_of_bound` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `Real.instMul` `NNReal.toReal` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `funLike`	`IsUniformEmbedding`	—	`AntilipschitzWith.isUniformEmbedding` `AddMonoidHomClass.antilipschitz_of_bound` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `continuousSemilinearMapClass` `uniformContinuous` `SeminormedAddCommGroup.to_isUniformAddGroup`

LinearEquiv

Definitions

Name	Category	Theorems
`toContinuousLinearEquivOfBounds` 📖	CompOp	—

LinearMap

Definitions

Name	Category	Theorems
`mkContinuous` 📖	CompOp	6 math math: `mkContinuous_apply`, `norm_mkContinuous₂_aux`, `PiTensorProduct.liftEquiv_apply`, `mkContinuous_coe`, `mkContinuous_norm_le'`, `mkContinuous_norm_le`
`mkContinuousOfExistsBound` 📖	CompOp	2 math math: `mkContinuousOfExistsBound_apply`, `mkContinuousOfExistsBound_coe`
`toContinuousLinearMap₁` 📖	CompOp	2 math math: `toContinuousLinearMap₁_coe`, `toContinuousLinearMap₁_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mkContinuousOfExistsBound_apply` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `instFunLike` `Real.instMul`	`ContinuousLinearMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousLinearMap.funLike` `mkContinuousOfExistsBound`	—	—
`mkContinuousOfExistsBound_coe` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `instFunLike` `Real.instMul`	`ContinuousLinearMap.toLinearMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `mkContinuousOfExistsBound`	—	—
`mkContinuous_apply` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `instFunLike` `Real.instMul`	`ContinuousLinearMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousLinearMap.funLike` `mkContinuous`	—	—
`mkContinuous_coe` 📖	mathematical	`Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `DFunLike.coe` `LinearMap` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `instFunLike` `Real.instMul`	`ContinuousLinearMap.toLinearMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `mkContinuous`	—	—
`toContinuousLinearMap₁_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `SeminormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Semiring.toModule` `ContinuousLinearMap.funLike` `toContinuousLinearMap₁` `LinearMap` `instFunLike`	—	—
`toContinuousLinearMap₁_coe` 📖	mathematical	—	`ContinuousLinearMap.toLinearMap` `Ring.toSemiring` `SeminormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Semiring.toModule` `toContinuousLinearMap₁`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_of_linear_of_bound` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`AddMonoidHomClass.continuous_of_bound` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`
`continuous_of_linear_of_boundₛₗ` 📖	mathematical	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Module.toDistribMulAction` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`AddMonoidHomClass.continuous_of_bound` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`

---

← Back to Index