Documentation Verification Report

ContinuousAffineMap

📁 Source: Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean

Statistics

Metric	Count
Definitions `hasNorm`, `instNormedAddCommGroup`, `instNormedSpace`, `toConstProdContinuousLinearMap`	4
Theorems `norm_comp_le`, `norm_contLinear_le`, `norm_def`, `norm_eq`, `norm_image_zero_le`, `toConstProdContinuousLinearMap_fst`, `toConstProdContinuousLinearMap_snd`	7
Total	11

ContinuousAffineMap

Definitions

Name	Category	Theorems
`hasNorm` 📖	CompOp	5 math math: `norm_def`, `norm_eq`, `norm_contLinear_le`, `norm_image_zero_le`, `norm_comp_le`
`instNormedAddCommGroup` 📖	CompOp	2 math math: `toConstProdContinuousLinearMap_fst`, `toConstProdContinuousLinearMap_snd`
`instNormedSpace` 📖	CompOp	—
`toConstProdContinuousLinearMap` 📖	CompOp	2 math math: `toConstProdContinuousLinearMap_fst`, `toConstProdContinuousLinearMap_snd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_comp_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousAffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `hasNorm` `comp` `Real.instAdd` `Real.instMul` `NormedAddCommGroup.toNorm` `DFunLike.coe` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`instIsTopologicalAddTorsor_1` `norm_def` `max_le_iff` `instIsTopologicalAddTorsor` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `decomp` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `zero_add` `le_imp_le_of_le_of_le` `norm_add_le` `le_refl` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `ContinuousLinearMap.le_opNorm` `RingHomIsometric.ids` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_contLinear_le` `norm_nonneg` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `norm_image_zero_le` `RingHomCompTriple.ids` `ContinuousLinearMap.opNorm_comp_le` `comp_contLinear` `le_add_iff_nonneg_right` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`norm_contLinear_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddCommGroup.toAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.hasOpNorm` `contLinear` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `instIsTopologicalAddTorsor_1` `ContinuousAffineMap` `hasNorm`	—	`le_max_right` `instIsTopologicalAddTorsor_1`
`norm_def` 📖	mathematical	—	`Norm.norm` `ContinuousAffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `hasNorm` `Real` `Real.instMax` `NormedAddCommGroup.toNorm` `DFunLike.coe` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.hasOpNorm` `contLinear` `instIsTopologicalAddTorsor_1`	—	—
`norm_eq` 📖	mathematical	`DFunLike.coe` `ContinuousAffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	`Norm.norm` `hasNorm` `ContinuousLinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `ContinuousLinearMap.hasOpNorm` `contLinear` `instIsTopologicalAddTorsor_1`	—	`instIsTopologicalAddTorsor_1` `norm_def` `norm_zero` `max_eq_right` `norm_nonneg` `RingHomIsometric.ids`
`norm_image_zero_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `DFunLike.coe` `ContinuousAffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `NormedAddCommGroup.toSeminormedAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `instFunLike` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `hasNorm`	—	`le_max_left`
`toConstProdContinuousLinearMap_fst` 📖	mathematical	—	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `DFunLike.coe` `LinearIsometryEquiv` `RingHomInvPair.ids` `ContinuousAffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `instNormedAddCommGroup` `Prod.seminormedAddCommGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instModuleOfSMulCommClassOfContinuousConstSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommGroup.toAddCommMonoid` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `Prod.instModule` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `toConstProdContinuousLinearMap` `instFunLike`	—	`RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`toConstProdContinuousLinearMap_snd` 📖	mathematical	—	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `DFunLike.coe` `LinearIsometryEquiv` `RingHomInvPair.ids` `ContinuousAffineMap` `NormedRing.toRing` `NormedCommRing.toNormedRing` `NormedField.toNormedCommRing` `NormedAddCommGroup.toAddCommGroup` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `instNormedAddCommGroup` `Prod.seminormedAddCommGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `instModuleOfSMulCommClassOfContinuousConstSMul` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommGroup.toAddCommMonoid` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `Prod.instModule` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.module` `EquivLike.toFunLike` `LinearIsometryEquiv.instEquivLike` `toConstProdContinuousLinearMap` `contLinear` `instIsTopologicalAddTorsor_1`	—	`RingHomInvPair.ids` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup`

---

← Back to Index