Documentation Verification Report

BoundedLinearMaps

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

Statistics

Metric	Count
Definitions `IsBoundedBilinearMap`, `deriv`, `linearDeriv`, `toContinuousLinearMap`, `IsBoundedLinearMap`, `toContinuousLinearMap`, `toLinearMap`	7
Theorems `clm_apply`, `clm_comp`, `continuousLinearMapCoprod`, `clm_apply`, `clm_comp`, `continuousLinearMapCoprod`, `isOpen`, `nhds`, `continuous₂`, `isBoundedBilinearMap`, `isBoundedLinearMap`, `isBoundedLinearMap_comp_left`, `isBoundedLinearMap_comp_right`, `mulLeftRight_isBoundedBilinear`, `clm_apply`, `clm_comp`, `continuousLinearMapCoprod`, `clm_apply`, `clm_comp`, `continuousLinearMapCoprod`, `add_left`, `add_right`, `continuous`, `continuous_left`, `continuous_right`, `deriv_apply`, `isBigO`, `isBigO'`, `isBigO_comp`, `isBoundedLinearMap_deriv`, `isBoundedLinearMap_left`, `isBoundedLinearMap_right`, `map_sub_left`, `map_sub_right`, `smul_left`, `smul_right`, `toContinuousLinearMap_apply`, `add`, `comp`, `continuous`, `fst`, `id`, `isBigO_comp`, `isBigO_id`, `isBigO_sub`, `isLinearMap_and_continuous_iff_isBoundedLinearMap`, `lim_zero_bounded_linear_map`, `neg`, `smul`, `snd`, `sub`, `tendsto`, `toIsLinearMap`, `zero`, `with_bound`, `isBoundedBilinearMap_apply`, `isBoundedBilinearMap_comp`, `isBoundedBilinearMap_compMultilinear`, `isBoundedBilinearMap_mul`, `isBoundedBilinearMap_smul`, `isBoundedBilinearMap_smulRight`, `isBoundedLinearMap_continuousMultilinearMap_comp_linear`, `isBoundedLinearMap_iff`, `isBoundedLinearMap_prod_multilinear`	64
Total	71

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_apply` 📖	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`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.funLike`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `comp₂` `RingHomIsometric.ids` `IsBoundedBilinearMap.continuous` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `isBoundedBilinearMap_apply`
`clm_comp` 📖	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`	`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` `ContinuousLinearMap.comp` `RingHomCompTriple.ids`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `comp₂` `RingHomIsometric.ids` `smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.continuous₂`
`continuousLinearMapCoprod` 📖	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`	`Continuous` `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` `ContinuousLinearMap.topologicalSpace` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.coprod` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `continuousOn_univ` `ContinuousOn.continuousLinearMapCoprod` `continuousOn`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_apply` 📖	mathematical	`ContinuousAt` `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`	`ContinuousAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.funLike`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `comp₂` `RingHomIsometric.ids` `Continuous.continuousAt` `IsBoundedBilinearMap.continuous` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `isBoundedBilinearMap_apply`
`clm_comp` 📖	mathematical	`ContinuousAt` `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`	`ContinuousAt` `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` `ContinuousLinearMap.comp` `RingHomCompTriple.ids`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `comp` `RingHomIsometric.ids` `smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Continuous.continuousAt` `ContinuousLinearMap.continuous₂` `prodMk`
`continuousLinearMapCoprod` 📖	mathematical	`ContinuousAt` `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`	`ContinuousAt` `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` `ContinuousLinearMap.topologicalSpace` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.coprod` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `fun_add` `RingHomIsometric.ids` `ContinuousLinearMap.topologicalAddGroup` `RingHomCompTriple.ids` `clm_comp` `continuousAt_const`

ContinuousLinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isOpen` 📖	mathematical	—	`IsOpen` `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` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Set.range` `ContinuousLinearEquiv` `RingHomInvPair.ids` `toContinuousLinearMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `isOpen_iff_mem_nhds` `Set.forall_mem_range` `IsOpen.mem_nhds` `RingHomCompTriple.ids` `IsBoundedBilinearMap.continuous_right` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `isBoundedBilinearMap_comp` `continuous_toFun` `Set.ext` `ContinuousLinearMap.ext` `apply_symm_apply` `IsOpen.preimage` `Units.isOpen` `instHasSummableGeomSeriesOfCompleteSpace` `ContinuousLinearMap.instCompleteSpace` `IsBoundedSMul.continuousSMul` `FrechetUrysohnSpace.to_sequentialSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `SeminormedAddCommGroup.to_isUniformAddGroup` `Set.mem_range_self`
`nhds` 📖	mathematical	—	`Set` `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` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Filter` `Filter.instMembership` `nhds` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `toContinuousLinearMap` `RingHomInvPair.ids` `Set.range` `ContinuousLinearEquiv`	—	`RingHomInvPair.ids` `IsOpen.mem_nhds` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `isOpen`

ContinuousLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous₂` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `funLike` `topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `module` `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` `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`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsBoundedBilinearMap.continuous` `isBoundedBilinearMap`
`isBoundedBilinearMap` 📖	mathematical	—	`IsBoundedBilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `funLike` `topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `module` `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` `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`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `map_add₂` `map_smul₂` `map_add` `map_smul` `RingHomIsometric.ids` `LT.lt.trans_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `le_max_right` `LE.le.trans` `le_opNorm₂` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `le_max_left` `norm_nonneg`
`isBoundedLinearMap` 📖	mathematical	—	`IsBoundedLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule` `DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `funLike`	—	`LinearMap.isLinear` `bound` `RingHomIsometric.ids`
`isBoundedLinearMap_comp_left` 📖	mathematical	—	`IsBoundedLinearMap` `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` `toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `module` `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` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `comp` `RingHomCompTriple.ids`	—	`IsBoundedBilinearMap.isBoundedLinearMap_right` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomCompTriple.ids` `isBoundedBilinearMap_comp`
`isBoundedLinearMap_comp_right` 📖	mathematical	—	`IsBoundedLinearMap` `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` `toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `module` `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` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `comp` `RingHomCompTriple.ids`	—	`IsBoundedBilinearMap.isBoundedLinearMap_left` `RingHomIsometric.ids` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomCompTriple.ids` `isBoundedBilinearMap_comp`
`mulLeftRight_isBoundedBilinear` 📖	mathematical	—	`IsBoundedBilinearMap` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `NonUnitalSeminormedRing.toPseudoMetricSpace` `SeminormedRing.toNonUnitalSeminormedRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalRing.toNonUnitalNonAssocRing` `NonUnitalSeminormedRing.toNonUnitalRing` `NormedSpace.toModule` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NormedAlgebra.toNormedSpace` `toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `SeminormedRing.toRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedSpace.toIsBoundedSMul` `SeminormedAddCommGroup.toPseudoMetricSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `DFunLike.coe` `topologicalSpace` `addCommMonoid` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `NonUnitalSeminormedRing.toIsTopologicalRing` `funLike` `addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `topologicalAddGroup` `ring` `toSeminormedRing` `smulCommClass` `continuousConstSMul` `mulLeftRight` `IsScalarTower.right` `Semifield.toCommSemiring` `NormedAlgebra.toAlgebra` `Algebra.to_smulCommClass`	—	`isBoundedBilinearMap` `RingHomIsometric.ids` `smulCommClass_self` `IsScalarTower.right` `Algebra.to_smulCommClass`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_apply` 📖	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`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.funLike`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `Continuous.comp_continuousOn` `RingHomIsometric.ids` `IsBoundedBilinearMap.continuous` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `isBoundedBilinearMap_apply` `prodMk`
`clm_comp` 📖	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`	`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` `ContinuousLinearMap.comp` `RingHomCompTriple.ids`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `Continuous.comp_continuousOn` `RingHomIsometric.ids` `smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.continuous₂` `prodMk`
`continuousLinearMapCoprod` 📖	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`	`ContinuousOn` `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` `ContinuousLinearMap.topologicalSpace` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.coprod` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `fun_add` `RingHomIsometric.ids` `ContinuousLinearMap.topologicalAddGroup` `RingHomCompTriple.ids` `clm_comp` `continuousOn_const`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_apply` 📖	mathematical	`ContinuousWithinAt` `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`	`ContinuousWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `ContinuousLinearMap.funLike`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAt.comp_continuousWithinAt` `RingHomIsometric.ids` `Continuous.continuousAt` `IsBoundedBilinearMap.continuous` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `isBoundedBilinearMap_apply` `prodMk`
`clm_comp` 📖	mathematical	`ContinuousWithinAt` `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`	`ContinuousWithinAt` `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` `ContinuousLinearMap.comp` `RingHomCompTriple.ids`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousAt.comp_continuousWithinAt` `RingHomIsometric.ids` `smulCommClass_self` `IsTopologicalAddGroup.toContinuousAdd` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Continuous.continuousAt` `ContinuousLinearMap.continuous₂` `prodMk`
`continuousLinearMapCoprod` 📖	mathematical	`ContinuousWithinAt` `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`	`ContinuousWithinAt` `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` `ContinuousLinearMap.topologicalSpace` `Prod.instAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.coprod` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `fun_add` `RingHomIsometric.ids` `ContinuousLinearMap.topologicalAddGroup` `RingHomCompTriple.ids` `clm_comp` `continuousWithinAt_const`

IsBoundedBilinearMap

Definitions

Name	Category	Theorems
`deriv` 📖	CompOp	7 math math: `hasFDerivAt`, `fderivWithin`, `isBoundedLinearMap_deriv`, `hasFDerivWithinAt`, `fderiv`, `hasStrictFDerivAt`, `deriv_apply`
`linearDeriv` 📖	CompOp	—
`toContinuousLinearMap` 📖	CompOp	1 math math: `toContinuousLinearMap_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_left` 📖	mathematical	`IsBoundedBilinearMap`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`add_right` 📖	mathematical	`IsBoundedBilinearMap`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`continuous` 📖	mathematical	`IsBoundedBilinearMap`	`Continuous` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`continuous_iff_continuousAt` `tendsto_sub_nhds_zero_iff` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Filter.Tendsto.add` `IsTopologicalAddGroup.toContinuousAdd` `Asymptotics.isLittleO_one_iff` `NormedDivisionRing.to_normOneClass` `one_mul` `Asymptotics.IsBigO.trans_isLittleO` `isBigO_comp` `Asymptotics.IsLittleO.mul_isBigO` `NormedDivisionRing.toNormMulClass` `Asymptotics.IsLittleO.norm_left` `Continuous.tendsto` `continuous_fst` `Asymptotics.IsBigO.norm_left` `Filter.Tendsto.isBigO_one` `continuous_snd` `Asymptotics.IsLittleO.const_mul_left` `Asymptotics.isLittleO_norm_left` `sub_self` `ContinuousAt.sub` `IsTopologicalAddGroup.to_continuousSub` `Continuous.continuousAt` `tendsto_const_nhds` `map_sub_left` `map_sub_right` `sub_add_sub_cancel` `zero_add`
`continuous_left` 📖	mathematical	`IsBoundedBilinearMap`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Continuous.comp` `continuous` `Continuous.prodMk` `continuous_id'` `continuous_const`
`continuous_right` 📖	mathematical	`IsBoundedBilinearMap`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Continuous.comp` `continuous` `Continuous.prodMk` `continuous_const` `continuous_id'`
`deriv_apply` 📖	mathematical	`IsBoundedBilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule`	`DFunLike.coe` `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` `ContinuousLinearMap.funLike` `deriv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup`	—	—
`isBigO` 📖	mathematical	`IsBoundedBilinearMap`	`Asymptotics.IsBigO` `Real` `SeminormedAddCommGroup.toNorm` `Real.norm` `Top.top` `Filter` `Filter.instTop` `Real.instMul` `Norm.norm`	—	`bound` `Asymptotics.IsBigO.of_bound` `Filter.Eventually.of_forall` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_norm` `mul_assoc`
`isBigO'` 📖	mathematical	`IsBoundedBilinearMap`	`Asymptotics.IsBigO` `Real` `SeminormedAddCommGroup.toNorm` `Real.norm` `Top.top` `Filter` `Filter.instTop` `Real.instMul` `Norm.norm` `Prod.toNorm`	—	`Asymptotics.IsBigO.trans` `isBigO` `Asymptotics.IsBigO.mul` `NormedDivisionRing.toNormMulClass` `Asymptotics.IsBigO.norm_norm` `Asymptotics.isBigO_fst_prod'` `Asymptotics.isBigO_snd_prod'`
`isBigO_comp` 📖	mathematical	`IsBoundedBilinearMap`	`Asymptotics.IsBigO` `Real` `SeminormedAddCommGroup.toNorm` `Real.norm` `Real.instMul` `Norm.norm`	—	`Asymptotics.IsBigO.comp_tendsto` `isBigO` `le_top`
`isBoundedLinearMap_deriv` 📖	mathematical	`IsBoundedBilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule`	`IsBoundedLinearMap` `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` `Prod.seminormedAddCommGroup` `ContinuousLinearMap.toSeminormedAddCommGroup` `Prod.normedSpace` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.module` `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` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `deriv`	—	`ContinuousLinearMap.isBoundedLinearMap` `RingHomIsometric.ids` `smulCommClass_self`
`isBoundedLinearMap_left` 📖	mathematical	`IsBoundedBilinearMap`	`IsBoundedLinearMap`	—	`isBoundedLinearMap_right` `symm`
`isBoundedLinearMap_right` 📖	mathematical	`IsBoundedBilinearMap`	`IsBoundedLinearMap`	—	`add_right` `smul_right` `bound` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `LE.le.trans` `max_cases` `le_refl` `le_imp_le_of_le_of_le` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `LT.lt.le` `le_of_lt` `norm_nonneg`
`map_sub_left` 📖	mathematical	`IsBoundedBilinearMap`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`IsLinearMap.map_sub` `IsBoundedLinearMap.toIsLinearMap` `isBoundedLinearMap_left`
`map_sub_right` 📖	mathematical	`IsBoundedBilinearMap`	`SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`IsLinearMap.map_sub` `IsBoundedLinearMap.toIsLinearMap` `isBoundedLinearMap_right`
`smul_left` 📖	mathematical	`IsBoundedBilinearMap`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`smul_right` 📖	mathematical	`IsBoundedBilinearMap`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`toContinuousLinearMap_apply` 📖	mathematical	`IsBoundedBilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `NormedSpace.toModule`	`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` `ContinuousLinearMap.funLike` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `ContinuousLinearMap.module` `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` `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` `toContinuousLinearMap`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`

IsBoundedLinearMap

Definitions

Name	Category	Theorems
`toContinuousLinearMap` 📖	CompOp	5 math math: `hasFDerivAtFilter`, `fderivWithin`, `hasFDerivAt`, `hasFDerivWithinAt`, `fderiv`
`toLinearMap` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`IsBoundedLinearMap`	`IsBoundedLinearMap` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`IsLinearMap.with_bound` `LinearMap.isLinear` `norm_add_le_of_le` `add_mul` `Distrib.rightDistribClass` `le_refl`
`comp` 📖	mathematical	`IsBoundedLinearMap`	`IsBoundedLinearMap`	—	`IsLinearMap.with_bound` `RingHomCompTriple.ids` `toIsLinearMap` `LinearMap.isLinear` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `mul_assoc`
`continuous` 📖	mathematical	`IsBoundedLinearMap`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`ContinuousLinearMap.continuous`
`fst` 📖	mathematical	—	`IsBoundedLinearMap` `Prod.seminormedAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`IsLinearMap.with_bound` `LinearMap.isLinear` `one_mul` `le_max_left`
`id` 📖	mathematical	—	`IsBoundedLinearMap`	—	`IsLinearMap.with_bound` `LinearMap.isLinear` `one_mul` `instReflLe`
`isBigO_comp` 📖	mathematical	`IsBoundedLinearMap`	`Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm`	—	`Asymptotics.IsBigO.comp_tendsto` `isBigO_id` `le_top`
`isBigO_id` 📖	mathematical	`IsBoundedLinearMap`	`Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm`	—	`bound` `Asymptotics.IsBigO.of_bound` `Filter.mem_of_superset` `Filter.univ_mem`
`isBigO_sub` 📖	mathematical	`IsBoundedLinearMap`	`Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`isBigO_comp`
`isLinearMap_and_continuous_iff_isBoundedLinearMap` 📖	mathematical	—	`IsLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `IsBoundedLinearMap`	—	`ContinuousLinearMap.isBoundedLinearMap` `toIsLinearMap` `continuous`
`lim_zero_bounded_linear_map` 📖	mathematical	`IsBoundedLinearMap`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`toIsLinearMap` `tendsto` `LinearMap.map_zero`
`neg` 📖	mathematical	`IsBoundedLinearMap`	`IsBoundedLinearMap` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`LinearMap.isLinear` `toIsLinearMap` `norm_neg` `bound`
`smul` 📖	mathematical	`IsBoundedLinearMap`	`IsBoundedLinearMap` `Function.hasSMul` `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` `SeminormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`IsLinearMap.with_bound` `LinearMap.isLinear` `norm_smul_le` `le_imp_le_of_le_of_le` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `norm_nonneg` `le_refl` `mul_assoc`
`snd` 📖	mathematical	—	`IsBoundedLinearMap` `Prod.seminormedAddCommGroup` `Prod.instModule` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`IsLinearMap.with_bound` `LinearMap.isLinear` `one_mul` `le_max_right`
`sub` 📖	mathematical	`IsBoundedLinearMap`	`IsBoundedLinearMap` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup`	—	`sub_eq_add_neg` `add` `neg`
`tendsto` 📖	mathematical	`IsBoundedLinearMap`	`Filter.Tendsto` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Continuous.tendsto` `ContinuousLinearMap.continuous`
`toIsLinearMap` 📖	mathematical	`IsBoundedLinearMap`	`IsLinearMap` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	—
`zero` 📖	mathematical	—	`IsBoundedLinearMap` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`IsLinearMap.with_bound` `LinearMap.isLinear` `norm_zero` `MulZeroClass.zero_mul` `instReflLe`

IsLinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`with_bound` 📖	mathematical	`IsLinearMap` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul`	`IsBoundedLinearMap`	—	`by_cases` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `LE.le.trans` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `zero_le_one` `norm_nonneg` `lt_of_not_ge`

(root)

Definitions

Name	Category	Theorems
`IsBoundedBilinearMap` 📖	CompData	10 math math: `ContinuousLinearMap.mulLeftRight_isBoundedBilinear`, `isBoundedBilinearMap_mul`, `isBoundedBilinearMap_comp`, `isBoundedBilinearMap_compMultilinear`, `ContinuousLinearMap.isBoundedBilinearMap`, `IsBoundedBilinearMap.symm`, `isBoundedBilinearMap_apply`, `isBoundedBilinearMap_smul`, `isBoundedBilinearMap_inner`, `isBoundedBilinearMap_smulRight`
`IsBoundedLinearMap` 📖	CompData	20 math math: `IsBoundedLinearMap.fst`, `IsBoundedLinearMap.comp`, `IsBoundedLinearMap.add`, `IsBoundedLinearMap.smul`, `ContinuousLinearMap.isBoundedLinearMap_comp_right`, `IsBoundedBilinearMap.isBoundedLinearMap_deriv`, `IsBoundedBilinearMap.isBoundedLinearMap_right`, `IsBoundedLinearMap.zero`, `IsBoundedLinearMap.snd`, `IsLinearMap.with_bound`, `ContinuousLinearMap.isBoundedLinearMap_comp_left`, `IsBoundedLinearMap.id`, `IsBoundedLinearMap.neg`, `isBoundedLinearMap_iff`, `IsBoundedBilinearMap.isBoundedLinearMap_left`, `ContinuousLinearMap.isBoundedLinearMap`, `IsBoundedLinearMap.sub`, `isBoundedLinearMap_continuousMultilinearMap_comp_linear`, `isBoundedLinearMap_prod_multilinear`, `IsBoundedLinearMap.isLinearMap_and_continuous_iff_isBoundedLinearMap`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBoundedBilinearMap_apply` 📖	mathematical	—	`IsBoundedBilinearMap` `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.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.module` `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` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `DFunLike.coe` `ContinuousLinearMap.funLike`	—	`ContinuousLinearMap.isBoundedBilinearMap` `RingHomIsometric.ids` `smulCommClass_self`
`isBoundedBilinearMap_comp` 📖	mathematical	—	`IsBoundedBilinearMap` `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.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.module` `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` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.comp` `RingHomCompTriple.ids`	—	`ContinuousLinearMap.isBoundedBilinearMap` `RingHomIsometric.ids` `smulCommClass_self`
`isBoundedBilinearMap_compMultilinear` 📖	mathematical	—	`IsBoundedBilinearMap` `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` `ContinuousMultilinearMap` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ContinuousLinearMap.toSeminormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.module` `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` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `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` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.seminormedAddCommGroup` `ContinuousMultilinearMap.instModule` `ContinuousLinearMap.compContinuousMultilinearMap`	—	`ContinuousLinearMap.isBoundedBilinearMap` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`isBoundedBilinearMap_mul` 📖	mathematical	—	`IsBoundedBilinearMap` `CommSemiring.toSemiring` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `SeminormedRing.toNonUnitalSeminormedRing` `Algebra.toModule` `Ring.toSemiring` `SeminormedRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`isBoundedBilinearMap_smul` `NonUnitalSeminormedRing.isBoundedSMul` `IsScalarTower.right`
`isBoundedBilinearMap_smul` 📖	mathematical	—	`IsBoundedBilinearMap` `CommSemiring.toSemiring` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `SeminormedRing.toNonUnitalSeminormedRing` `Algebra.toModule` `Ring.toSemiring` `SeminormedRing.toRing` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup`	—	`add_smul` `smul_assoc` `smul_add` `SMulCommClass.smul_comm` `IsScalarTower.to_smulCommClass'` `one_pos` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `one_mul` `le_imp_le_of_le_of_le` `norm_smul_le` `le_refl`
`isBoundedBilinearMap_smulRight` 📖	mathematical	—	`IsBoundedBilinearMap` `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` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NormedSpace.toModule` `Semiring.toModule` `ContinuousLinearMap.toSeminormedAddCommGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedField.toNormedSpace` `RingHomIsometric.ids` `ContinuousLinearMap.module` `Algebra.to_smulCommClass` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `SeparatelyContinuousMul.to_continuousSMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `IsSemitopologicalSemiring.toSeparatelyContinuousMul` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.toDivisionRing` `NormedField.toNormedDivisionRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `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` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.smulRight` `IsScalarTower.left` `IsBoundedSMul.continuousSMul`	—	`ContinuousLinearMap.isBoundedBilinearMap` `RingHomIsometric.ids` `Algebra.to_smulCommClass` `smulCommClass_self`
`isBoundedLinearMap_continuousMultilinearMap_comp_linear` 📖	mathematical	—	`IsBoundedLinearMap` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ContinuousMultilinearMap.seminormedAddCommGroup'` `ContinuousMultilinearMap.instModule` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousMultilinearMap.compContinuousLinearMap`	—	`ContinuousLinearMap.isBoundedLinearMap` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul`
`isBoundedLinearMap_iff` 📖	mathematical	—	`IsBoundedLinearMap` `IsLinearMap` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `Real` `Real.instLT` `Real.instZero` `Real.instLE` `Norm.norm` `SeminormedAddCommGroup.toNorm` `Real.instMul`	—	`IsBoundedLinearMap.toIsLinearMap` `IsBoundedLinearMap.bound`
`isBoundedLinearMap_prod_multilinear` 📖	mathematical	—	`IsBoundedLinearMap` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Prod.instAddCommMonoid` `Prod.instModule` `instTopologicalSpaceProd` `Prod.seminormedAddCommGroup` `ContinuousMultilinearMap.seminormedAddCommGroup` `ContinuousMultilinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousMultilinearMap.instModule` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction` `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` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Prod.normedSpace` `Prod.continuousConstSMul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Prod.smulCommClass` `ContinuousMultilinearMap.prod`	—	`ContinuousLinearMap.isBoundedLinearMap` `smulCommClass_self` `Prod.smulCommClass` `RingHomInvPair.ids` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Prod.continuousConstSMul`

---

← Back to Index