Documentation Verification Report

Prod

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

Statistics

Metric	Count
Definitions `prodMapL`, `prodₗᵢ`	2
Theorems `prod_mapL`, `prod_map_equivL`, `norm_fst`, `norm_fst_le`, `norm_snd`, `norm_snd_le`, `opNNNorm_prod`, `opNorm_prod`, `prodMapL_apply`, `prod_mapL`, `prod_map_equivL`	11
Total	13

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_mapL` 📖	mathematical	`Continuous` `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` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	`instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `Prod.instAddCommGroup` `Prod.instIsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousLinearMap.prodMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `comp` `Prod.instIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `Prod.continuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Prod.smulCommClass` `Prod.continuousConstSMul` `ContinuousLinearMap.continuous` `prodMk`
`prod_map_equivL` 📖	mathematical	`Continuous` `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` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids`	`instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `Prod.instAddCommGroup` `Prod.instIsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousLinearEquiv.prodCongr`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `comp` `Prod.instIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `Prod.continuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Prod.smulCommClass` `Prod.continuousConstSMul` `ContinuousLinearMap.continuous` `prodMk`

ContinuousLinearMap

Definitions

Name	Category	Theorems
`prodMapL` 📖	CompOp	1 math math: `prodMapL_apply`
`prodₗᵢ` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_fst` 📖	mathematical	—	`Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instAddCommMonoid` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `NormedSpace.toModule` `hasOpNorm` `Prod.seminormedAddCommGroup` `Prod.normedSpace` `fst` `Real` `Real.instOne`	—	`le_antisymm` `norm_fst_le` `exists_ne` `le_opNorm` `RingHomIsometric.ids` `mul_le_mul_iff_of_pos_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `one_mul` `max_eq_left` `norm_nonneg` `norm_zero`
`norm_fst_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `NormedSpace.toModule` `hasOpNorm` `Prod.seminormedAddCommGroup` `Prod.normedSpace` `fst` `Real.instOne`	—	`opNorm_le_bound` `zero_le_one` `Real.instZeroLEOneClass` `one_mul` `le_max_left`
`norm_snd` 📖	mathematical	—	`Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Prod.instModule` `NormedSpace.toModule` `hasOpNorm` `Prod.seminormedAddCommGroup` `Prod.normedSpace` `snd` `Real` `Real.instOne`	—	`le_antisymm` `norm_snd_le` `exists_ne` `le_opNorm` `RingHomIsometric.ids` `mul_le_mul_iff_of_pos_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `norm_pos_iff` `one_mul` `max_eq_right` `norm_nonneg` `norm_zero`
`norm_snd_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Prod.instModule` `NormedSpace.toModule` `hasOpNorm` `Prod.seminormedAddCommGroup` `Prod.normedSpace` `snd` `Real.instOne`	—	`opNorm_le_bound` `zero_le_one` `Real.instZeroLEOneClass` `one_mul` `le_max_right`
`opNNNorm_prod` 📖	mathematical	—	`NNNorm.nnnorm` `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` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `NormedSpace.toModule` `Prod.instModule` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `toSeminormedAddCommGroup` `Prod.seminormedAddCommGroup` `Prod.normedSpace` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `prod` `Prod.seminormedAddGroup`	—	`RingHomIsometric.ids` `opNorm_prod`
`opNorm_prod` 📖	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` `instTopologicalSpaceProd` `Prod.instAddCommMonoid` `NormedSpace.toModule` `Prod.instModule` `hasOpNorm` `Prod.seminormedAddCommGroup` `Prod.normedSpace` `prod` `Prod.toNorm`	—	`le_antisymm` `opNorm_le_bound` `norm_nonneg` `RingHomIsometric.ids` `max_mul_of_nonneg` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `max_le_max` `le_opNorm` `max_le` `LE.le.trans` `le_max_left` `le_max_right`
`prodMapL_apply` 📖	mathematical	—	`DFunLike.coe` `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` `NormedSpace.toModule` `instTopologicalSpaceProd` `topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Prod.instAddCommMonoid` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `Prod.instModule` `Prod.instAddCommGroup` `Prod.instIsTopologicalAddGroup` `AddCommGroup.toAddGroup` `Prod.continuousAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddCommMonoid.toAddMonoid` `module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `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.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Prod.continuousConstSMul` `funLike` `prodMapL` `prodMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `Prod.instIsTopologicalAddGroup` `Prod.continuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Prod.smulCommClass` `Prod.continuousConstSMul`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_mapL` 📖	mathematical	`ContinuousOn` `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` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup`	`instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `Prod.instAddCommGroup` `Prod.instIsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousLinearMap.prodMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `Continuous.comp_continuousOn` `Prod.instIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `Prod.continuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Prod.smulCommClass` `Prod.continuousConstSMul` `ContinuousLinearMap.continuous` `prodMk`
`prod_map_equivL` 📖	mathematical	`ContinuousOn` `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` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids`	`instTopologicalSpaceProd` `Prod.instAddCommMonoid` `Prod.instModule` `Prod.instAddCommGroup` `Prod.instIsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousLinearEquiv.prodCongr`	—	`RingHomInvPair.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `prod_mapL`

---

← Back to Index