Documentation Verification Report

Hom

📁 Source: Mathlib/Geometry/Manifold/VectorBundle/Hom.lean

Statistics

Metric	Count
Definitions	0
Theorems `isContMDiff`, `clm_bundle_apply`, `clm_bundle_apply₂`, `clm_apply_of_inCoordinates`, `clm_bundle_apply`, `clm_bundle_apply₂`, `clm_bundle_apply`, `clm_bundle_apply₂`, `continuousLinearMap`, `clm_apply_of_inCoordinates`, `clm_bundle_apply`, `clm_bundle_apply₂`, `clm_bundle_apply`, `clm_bundle_apply₂`, `clm_bundle_apply`, `clm_bundle_apply₂`, `clm_bundle_apply`, `clm_bundle_apply₂`, `clm_bundle_apply`, `clm_bundle_apply₂`, `contMDiffAt_hom_bundle`, `contMDiffOn_continuousLinearMapCoordChange`, `contMDiffWithinAt_hom_bundle`, `hom_chart`, `mdifferentiableAt_hom_bundle`, `mdifferentiableOn_continuousLinearMapCoordChange`, `mdifferentiableWithinAt_hom_bundle`	27
Total	27

Bundle.ContinuousLinearMap.vectorPrebundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isContMDiff` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`VectorPrebundle.IsContMDiff` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `Field.toCommRing` `DistribMulAction.toMulAction` `ContinuousSMul.continuousConstSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.vectorPrebundle`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `trivialization_linear` `contMDiffOn_continuousLinearMapCoordChange` `Pretrivialization.continuousLinearMapCoordChange_apply`

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_bundle_apply` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiff` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `ContMDiffAt.clm_bundle_apply`
`clm_bundle_apply₂` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiff` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `Prod.normedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `ContinuousLinearMap.smulCommClass` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `ContinuousSMul.continuousConstSMul` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `ContMDiffAt.clm_bundle_apply₂`

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_apply_of_inCoordinates` 📖	mathematical	`ContMDiffAt` `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` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `modelWithCornersSelf` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearMap.inCoordinates` `AddCommGroup.toAddCommMonoid` `Prod.normedAddCommGroup` `Prod.normedSpace` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `Bundle.TotalSpace` `FiberBundle.chartedSpace`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `contMDiffWithinAt_univ` `ContMDiffWithinAt.clm_apply_of_inCoordinates`
`clm_bundle_apply` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiffAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `ContMDiffWithinAt.clm_bundle_apply`
`clm_bundle_apply₂` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiffAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `Prod.normedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `ContinuousLinearMap.smulCommClass` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `ContinuousSMul.continuousConstSMul` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `ContMDiffWithinAt.clm_bundle_apply₂`

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_bundle_apply` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiffOn` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `ContMDiffWithinAt.clm_bundle_apply`
`clm_bundle_apply₂` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiffOn` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `Prod.normedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `ContinuousLinearMap.smulCommClass` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `ContinuousSMul.continuousConstSMul` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `ContMDiffWithinAt.clm_bundle_apply₂`

ContMDiffVectorBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousLinearMap` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`ContMDiffVectorBundle` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `ContinuousSMul.continuousConstSMul` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.ContinuousLinearMap.vectorBundle`	—	`VectorPrebundle.contMDiffVectorBundle` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `RingHomIsometric.ids` `Bundle.ContinuousLinearMap.vectorPrebundle.isContMDiff`

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_apply_of_inCoordinates` 📖	mathematical	`ContMDiffWithinAt` `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` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `modelWithCornersSelf` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearMap.inCoordinates` `AddCommGroup.toAddCommMonoid` `Prod.normedAddCommGroup` `Prod.normedSpace` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `Bundle.TotalSpace` `FiberBundle.chartedSpace`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `contMDiffWithinAt_insert_self` `Bundle.contMDiffWithinAt_totalSpace` `congr_of_eventuallyEq_of_mem` `clm_apply` `continuousWithinAt` `IsOpen.mem_nhds` `Trivialization.open_baseSet` `FiberBundle.mem_baseSet_trivializationAt'` `Filter.mp_mem` `Filter.univ_mem'` `RingHomCompTriple.right_ids` `RingHomInvPair.ids` `trivialization_linear` `instMemTrivializationAtlasTrivializationAt` `RingHomCompTriple.ids` `ContinuousLinearMap.inCoordinates_eq` `Set.mem_insert`
`clm_bundle_apply` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiffWithinAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `clm_apply_of_inCoordinates` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`clm_bundle_apply₂` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `ContMDiffWithinAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `Prod.normedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `ContinuousLinearMap.smulCommClass` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `ContinuousSMul.continuousConstSMul` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `clm_bundle_apply`

MDifferentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_bundle_apply` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MDifferentiable` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `MDifferentiableAt.clm_bundle_apply`
`clm_bundle_apply₂` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MDifferentiable` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `Prod.normedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `ContinuousLinearMap.smulCommClass` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `ContinuousSMul.continuousConstSMul` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `MDifferentiableAt.clm_bundle_apply₂`

MDifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_bundle_apply` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MDifferentiableAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `MDifferentiableWithinAt.clm_bundle_apply`
`clm_bundle_apply₂` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MDifferentiableAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `Prod.normedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `ContinuousLinearMap.smulCommClass` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `ContinuousSMul.continuousConstSMul` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `MDifferentiableWithinAt.clm_bundle_apply₂`

MDifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_bundle_apply` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MDifferentiableOn` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `MDifferentiableWithinAt.clm_bundle_apply`
`clm_bundle_apply₂` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MDifferentiableOn` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `Prod.normedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `ContinuousLinearMap.smulCommClass` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `ContinuousSMul.continuousConstSMul` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `MDifferentiableWithinAt.clm_bundle_apply₂`

MDifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_bundle_apply` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MDifferentiableWithinAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`RingHomIsometric.ids` `smulCommClass_self` `clm_apply_of_inCoordinates` `SeminormedAddCommGroup.toIsTopologicalAddGroup`
`clm_bundle_apply₂` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MDifferentiableWithinAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `Prod.normedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `ContinuousLinearMap.smulCommClass` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `ContinuousSMul.continuousConstSMul` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`DFunLike.coe` `ContinuousLinearMap.funLike`	—	`IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `ContinuousSMul.continuousConstSMul` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `RingHomIsometric.ids` `ContinuousLinearMap.smulCommClass` `Bundle.ContinuousLinearMap.vectorBundle` `ContinuousLinearMap.topologicalAddGroup` `ContinuousLinearMap.continuousSMul` `RingHomSurjective.ids` `clm_bundle_apply`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contMDiffAt_hom_bundle` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`ContMDiffAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.proj` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearMap.inCoordinates` `Bundle.TotalSpace.snd`	—	`Bundle.contMDiffAt_totalSpace` `RingHomIsometric.ids` `smulCommClass_self`
`contMDiffOn_continuousLinearMapCoordChange` 📖	mathematical	—	`ContMDiffOn` `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` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `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` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `ContinuousLinearMap.smulCommClass` `AddCommGroup.toAddCommMonoid` `modelWithCornersSelf` `Field.toCommRing` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousLinearMap.topologicalAddGroup` `chartedSpaceSelf` `Pretrivialization.continuousLinearMapCoordChange` `trivialization_linear` `Set` `Set.instInter` `Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `trivialization_linear` `contMDiffOn_coordChangeL` `ContMDiffOn.cle_arrowCongr` `ContMDiffOn.mono`
`contMDiffWithinAt_hom_bundle` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`ContMDiffWithinAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.proj` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearMap.inCoordinates` `Bundle.TotalSpace.snd`	—	`Bundle.contMDiffWithinAt_totalSpace` `RingHomIsometric.ids` `smulCommClass_self`
`hom_chart` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`OpenPartialHomeomorph.toFun'` `Bundle.TotalSpace` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ModelProd` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `RingHomIsometric.ids` `instTopologicalSpaceModelProd` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartAt` `FiberBundle.chartedSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.proj` `ContinuousLinearMap.inCoordinates` `Bundle.TotalSpace.snd`	—	`RingHomIsometric.ids` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `FiberBundle.chartedSpace_chartAt` `OpenPartialHomeomorph.trans_apply` `OpenPartialHomeomorph.prod_apply` `Trivialization.coe_coe` `OpenPartialHomeomorph.refl_apply` `hom_trivializationAt_apply`
`mdifferentiableAt_hom_bundle` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`MDifferentiableAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.proj` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearMap.inCoordinates` `Bundle.TotalSpace.snd`	—	`mdifferentiableAt_totalSpace` `RingHomIsometric.ids` `smulCommClass_self`
`mdifferentiableOn_continuousLinearMapCoordChange` 📖	mathematical	—	`MDifferentiableOn` `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` `ContinuousLinearMap.topologicalSpace` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `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` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toIsBoundedSMul` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `ContinuousLinearMap.toNormedSpace` `ContinuousLinearMap.toSeminormedAddCommGroup` `ContinuousLinearMap.smulCommClass` `AddCommGroup.toAddCommMonoid` `modelWithCornersSelf` `Field.toCommRing` `ContinuousLinearMap.addCommGroup` `NormedRing.toRing` `NormedCommRing.toNormedRing` `ContinuousLinearMap.topologicalAddGroup` `chartedSpaceSelf` `Pretrivialization.continuousLinearMapCoordChange` `trivialization_linear` `Set` `Set.instInter` `Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `trivialization_linear` `ContMDiffOn.mdifferentiableOn` `contMDiffOn_coordChangeL` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `MDifferentiableOn.cle_arrowCongr` `MDifferentiableOn.mono`
`mdifferentiableWithinAt_hom_bundle` 📖	mathematical	`IsTopologicalAddGroup` `AddCommGroup.toAddGroup` `ContinuousSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing`	`MDifferentiableWithinAt` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Prod.normedAddCommGroup` `ContinuousLinearMap.toNormedAddCommGroup` `RingHomIsometric.ids` `Prod.normedSpace` `ContinuousLinearMap.toNormedSpace` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Ring.toSemiring` `CommRing.toRing` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace` `FiberBundle.chartedSpace` `ContinuousLinearMap.topologicalSpace` `Bundle.ContinuousLinearMap.fiberBundle` `Bundle.TotalSpace.proj` `SeminormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `chartedSpaceSelf` `ContinuousLinearMap.inCoordinates` `Bundle.TotalSpace.snd`	—	`mdifferentiableWithinAt_totalSpace` `RingHomIsometric.ids` `smulCommClass_self`

---

← Back to Index