MDifferentiable

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

Statistics

Metric	Count
Definitions	0
Theorems `mdifferentiableAt_proj`, `mdifferentiableAt_zeroSection`, `mdifferentiableOn_proj`, `mdifferentiableOn_zeroSection`, `mdifferentiableWithinAt_proj`, `mdifferentiableWithinAt_zeroSection`, `mdifferentiable_proj`, `mdifferentiable_zeroSection`, `coordChange`, `coordChangeL`, `finsum_section_of_locallyFinite`, `sum_section`, `sum_section_of_locallyFinite`, `clm_apply_of_inCoordinates`, `coordChange`, `coordChangeL`, `finsum_section_of_locallyFinite`, `smul_const_section`, `smul_section`, `sum_section`, `sum_section_of_locallyFinite`, `coordChange`, `coordChangeL`, `finsum_section_of_locallyFinite`, `smul_const_section`, `smul_section`, `smul_section_of_tsupport`, `sum_section`, `sum_section_of_locallyFinite`, `change_section_trivialization`, `clm_apply_of_inCoordinates`, `coordChange`, `coordChangeL`, `finsum_section_of_locallyFinite`, `smul_section`, `sum_section`, `sum_section_of_locallyFinite`, `mdifferentiableAt_section_iff`, `mdifferentiableAt_snd_comp_iff₂`, `mdifferentiableAt_totalSpace_iff`, `mdifferentiableOn_section_baseSet_iff`, `mdifferentiableOn_section_iff`, `mdifferentiableWithinAt_section_iff`, `mdifferentiableWithinAt_snd_comp_iff₂`, `mdifferentiableWithinAt_totalSpace_iff`, `mDifferentiableOn_sub_section`, `mdifferentiableAt_add_section`, `mdifferentiableAt_coordChangeL`, `mdifferentiableAt_neg_section`, `mdifferentiableAt_section`, `mdifferentiableAt_sub_section`, `mdifferentiableAt_totalSpace`, `mdifferentiableOn_add_section`, `mdifferentiableOn_coordChangeL`, `mdifferentiableOn_neg_section`, `mdifferentiableOn_symm_coordChangeL`, `mdifferentiableWithinAt_add_section`, `mdifferentiableWithinAt_neg_section`, `mdifferentiableWithinAt_section`, `mdifferentiableWithinAt_smul_const_section`, `mdifferentiableWithinAt_sub_section`, `mdifferentiableWithinAt_totalSpace`, `mdifferentiable_add_section`, `mdifferentiable_neg_section`, `mdifferentiable_smul_const_section`, `mdifferentiable_smul_section`, `mdifferentiable_sub_section`	67
Total	67

Bundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mdifferentiableAt_proj` 📖	mathematical	—	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `TotalSpace` `FiberBundle.chartedSpace` `TotalSpace.proj`	—	`MDifferentiable.mdifferentiableAt` `mdifferentiable_proj`
`mdifferentiableAt_zeroSection` 📖	mathematical	—	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `TotalSpace` `FiberBundle.chartedSpace` `zeroSection` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`MDifferentiable.mdifferentiableAt` `mdifferentiable_zeroSection`
`mdifferentiableOn_proj` 📖	mathematical	—	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `TotalSpace` `FiberBundle.chartedSpace` `TotalSpace.proj`	—	`MDifferentiable.mdifferentiableOn` `mdifferentiable_proj`
`mdifferentiableOn_zeroSection` 📖	mathematical	—	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `TotalSpace` `FiberBundle.chartedSpace` `zeroSection` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`MDifferentiable.mdifferentiableOn` `mdifferentiable_zeroSection`
`mdifferentiableWithinAt_proj` 📖	mathematical	—	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `TotalSpace` `FiberBundle.chartedSpace` `TotalSpace.proj`	—	`MDifferentiableAt.mdifferentiableWithinAt` `mdifferentiableAt_proj`
`mdifferentiableWithinAt_zeroSection` 📖	mathematical	—	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `TotalSpace` `FiberBundle.chartedSpace` `zeroSection` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`MDifferentiableAt.mdifferentiableWithinAt` `mdifferentiable_zeroSection`
`mdifferentiable_proj` 📖	mathematical	—	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `TotalSpace` `FiberBundle.chartedSpace` `TotalSpace.proj`	—	`mdifferentiableAt_id` `mdifferentiableAt_totalSpace`
`mdifferentiable_zeroSection` 📖	mathematical	—	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `TotalSpace` `FiberBundle.chartedSpace` `zeroSection` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid`	—	`mdifferentiableAt_section` `MDifferentiableAt.congr_of_eventuallyEq` `mdifferentiableAt_const` `Filter.mp_mem` `IsOpen.mem_nhds` `Trivialization.open_baseSet` `FiberBundle.mem_baseSet_trivializationAt` `Filter.univ_mem'` `Trivialization.zeroSection` `trivialization_linear` `instMemTrivializationAtlasTrivializationAt`

MDifferentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coordChange` 📖	mathematical	`MDifferentiable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Set` `Set.instMembership` `Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	`Trivialization.coordChange`	—	`MDifferentiableAt.coordChange`
`coordChangeL` 📖	mathematical	`MDifferentiable` `Set` `Set.instMembership` `Trivialization.baseSet` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Trivialization.coordChangeL` `trivialization_linear`	—	`MDifferentiableAt.coordChangeL`
`finsum_section_of_locallyFinite` 📖	mathematical	`LocallyFinite` `setOf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`finsum` `AddCommGroup.toAddCommMonoid`	—	`MDifferentiableAt.finsum_section_of_locallyFinite`
`sum_section` 📖	mathematical	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Finset.sum` `AddCommGroup.toAddCommMonoid`	—	`MDifferentiableAt.sum_section`
`sum_section_of_locallyFinite` 📖	mathematical	`LocallyFinite` `setOf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`tsum` `AddCommGroup.toAddCommMonoid` `SummationFilter.unconditional`	—	`MDifferentiableAt.sum_section_of_locallyFinite`

MDifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`clm_apply_of_inCoordinates` 📖	mathematical	`MDifferentiableAt` `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` `mdifferentiableWithinAt_univ` `MDifferentiableWithinAt.clm_apply_of_inCoordinates`
`coordChange` 📖	mathematical	`MDifferentiableAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Set` `Set.instMembership` `Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	`Trivialization.coordChange`	—	`MDifferentiableWithinAt.coordChange`
`coordChangeL` 📖	mathematical	`MDifferentiableAt` `Set` `Set.instMembership` `Trivialization.baseSet` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Trivialization.coordChangeL` `trivialization_linear`	—	`MDifferentiableWithinAt.coordChangeL`
`finsum_section_of_locallyFinite` 📖	mathematical	`LocallyFinite` `setOf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`finsum` `AddCommGroup.toAddCommMonoid`	—	`MDifferentiableWithinAt.finsum_section_of_locallyFinite`
`smul_const_section` 📖	mathematical	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_section` `mdifferentiableAt_const`
`smul_section` 📖	mathematical	`MDifferentiableAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `chartedSpaceSelf` `Prod.normedAddCommGroup` `Prod.normedSpace` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`mdifferentiableWithinAt_univ` `MDifferentiableWithinAt.smul_section`
`sum_section` 📖	mathematical	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Finset.sum` `AddCommGroup.toAddCommMonoid`	—	`MDifferentiableWithinAt.sum_section`
`sum_section_of_locallyFinite` 📖	mathematical	`LocallyFinite` `setOf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`tsum` `AddCommGroup.toAddCommMonoid` `SummationFilter.unconditional`	—	`MDifferentiableWithinAt.sum_section_of_locallyFinite`

MDifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coordChange` 📖	mathematical	`MDifferentiableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Set.MapsTo` `Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	`Trivialization.coordChange`	—	`MDifferentiableWithinAt.coordChange`
`coordChangeL` 📖	mathematical	`MDifferentiableOn` `Set.MapsTo` `Trivialization.baseSet` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Trivialization.coordChangeL` `trivialization_linear`	—	`MDifferentiableWithinAt.coordChangeL`
`finsum_section_of_locallyFinite` 📖	mathematical	`LocallyFinite` `setOf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`finsum` `AddCommGroup.toAddCommMonoid`	—	`MDifferentiableWithinAt.finsum_section_of_locallyFinite`
`smul_const_section` 📖	mathematical	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`smul_section` `mdifferentiableOn_const`
`smul_section` 📖	mathematical	`MDifferentiableOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `chartedSpaceSelf` `Prod.normedAddCommGroup` `Prod.normedSpace` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`MDifferentiableWithinAt.smul_section`
`smul_section_of_tsupport` 📖	mathematical	`MDifferentiableOn` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `chartedSpaceSelf` `IsOpen` `Set` `Set.instHasSubset` `tsupport` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `Prod.normedAddCommGroup` `Prod.normedSpace` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`MDifferentiable` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`mdifferentiable_of_mdifferentiableOn_union_of_isOpen` `smul_section` `congr` `MDifferentiable.mdifferentiableOn` `Bundle.mdifferentiable_zeroSection` `image_eq_zero_of_notMem_tsupport` `zero_smul` `Set.compl_subset_iff_union` `Set.compl_subset_compl` `isOpen_compl_iff` `isClosed_tsupport`
`sum_section` 📖	mathematical	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Finset.sum` `AddCommGroup.toAddCommMonoid`	—	`MDifferentiableWithinAt.sum_section`
`sum_section_of_locallyFinite` 📖	mathematical	`LocallyFinite` `setOf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`tsum` `AddCommGroup.toAddCommMonoid` `SummationFilter.unconditional`	—	`MDifferentiableWithinAt.sum_section_of_locallyFinite`

MDifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`change_section_trivialization` 📖	—	`MDifferentiableWithinAt` `Bundle.TotalSpace` `Bundle.TotalSpace.proj` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Trivialization.toFun'` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceProd` `Trivialization.toOpenPartialHomeomorph`	—	—	`congr_of_eventuallyEq` `coordChange` `Trivialization.mem_source` `Filter.mp_mem` `continuousWithinAt` `IsOpen.mem_nhds` `Trivialization.open_baseSet` `Filter.univ_mem'` `Trivialization.coordChange_apply_snd`
`clm_apply_of_inCoordinates` 📖	mathematical	`MDifferentiableWithinAt` `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` `mdifferentiableWithinAt_totalSpace` `congr_of_eventuallyEq_insert` `clm_apply` `continuousWithinAt` `insert` `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`
`coordChange` 📖	mathematical	`MDifferentiableWithinAt` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `chartedSpaceSelf` `Set` `Set.instMembership` `Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	`Trivialization.coordChange`	—	`congr_of_eventuallyEq` `RingHomInvPair.ids` `trivialization_linear` `clm_apply` `coordChangeL` `IsOpen.mem_nhds` `IsOpen.inter` `Trivialization.open_baseSet` `Filter.mp_mem` `continuousWithinAt` `Filter.univ_mem'` `Trivialization.coordChangeL_apply'`
`coordChangeL` 📖	mathematical	`MDifferentiableWithinAt` `Set` `Set.instMembership` `Trivialization.baseSet` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj`	`ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Trivialization.coordChangeL` `trivialization_linear`	—	`MDifferentiableAt.comp_mdifferentiableWithinAt` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `trivialization_linear` `mdifferentiableAt_coordChangeL`
`finsum_section_of_locallyFinite` 📖	mathematical	`LocallyFinite` `setOf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`finsum` `AddCommGroup.toAddCommMonoid`	—	`congr'` `sum_section_of_locallyFinite` `Set.mem_setOf` `mem_of_mem_nhds` `tsum_eq_finsum` `SummationFilter.instLeAtTopUnconditional` `Set.Finite.subset`
`smul_section` 📖	mathematical	`MDifferentiableWithinAt` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `chartedSpaceSelf` `Prod.normedAddCommGroup` `Prod.normedSpace` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`mdifferentiableWithinAt_section` `congr_of_eventuallyEq` `smul` `Filter.eventually_of_mem` `mem_nhdsWithin_of_mem_nhds` `IsOpen.mem_nhds` `Trivialization.open_baseSet` `FiberBundle.mem_baseSet_trivializationAt` `IsLinearMap.map_smul` `Trivialization.linear` `trivialization_linear` `instMemTrivializationAtlasTrivializationAt` `FiberBundle.mem_baseSet_trivializationAt'`
`sum_section` 📖	mathematical	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Finset.sum` `AddCommGroup.toAddCommMonoid`	—	`Finset.induction_on` `ContMDiffWithinAt.mdifferentiableWithinAt` `Bundle.contMDiffWithinAt_zeroSection` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero` `Finset.sum_insert` `mdifferentiableWithinAt_add_section`
`sum_section_of_locallyFinite` 📖	mathematical	`LocallyFinite` `setOf` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`tsum` `AddCommGroup.toAddCommMonoid` `SummationFilter.unconditional`	—	`sum_section` `mono` `Set.inter_subset_left` `mdifferentiableWithinAt_inter` `congr'` `tsum_eq_sum'` `SummationFilter.instLeAtTopUnconditional` `Function.support_subset_iff'` `Set.mem_toFinset` `Set.inter_subset_right` `mem_of_mem_nhds`

Trivialization

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mdifferentiableAt_section_iff` 📖	mathematical	`Set` `Set.instMembership` `baseSet` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj`	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `chartedSpaceSelf` `toFun'`	—	`mdifferentiableWithinAt_section_iff`
`mdifferentiableAt_snd_comp_iff₂` 📖	mathematical	`Bundle.TotalSpace` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `MDifferentiableAt`	`modelWithCornersSelf` `chartedSpaceSelf` `toFun'`	—	`mdifferentiableWithinAt_snd_comp_iff₂`
`mdifferentiableAt_totalSpace_iff` 📖	mathematical	`Bundle.TotalSpace` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `toOpenPartialHomeomorph` `Bundle.TotalSpace.proj`	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `FiberBundle.chartedSpace` `chartedSpaceSelf` `toFun'`	—	`mdifferentiableAt_totalSpace` `mdifferentiableAt_snd_comp_iff₂` `instMemTrivializationAtlasTrivializationAt` `FiberBundle.mem_trivializationAt_proj_source`
`mdifferentiableOn_section_baseSet_iff` 📖	mathematical	—	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `baseSet` `Bundle.TotalSpace.proj` `chartedSpaceSelf` `toFun'`	—	`mdifferentiableOn_section_iff` `open_baseSet` `subset_rfl` `Set.instReflSubset`
`mdifferentiableOn_section_iff` 📖	mathematical	`IsOpen` `Set` `Set.instHasSubset` `baseSet` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj`	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `chartedSpaceSelf` `toFun'`	—	`MDifferentiableWithinAt.mdifferentiableAt` `IsOpen.mem_nhds` `MDifferentiableAt.mdifferentiableWithinAt` `mdifferentiableAt_section_iff`
`mdifferentiableWithinAt_section_iff` 📖	mathematical	`Set` `Set.instMembership` `baseSet` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj`	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `chartedSpaceSelf` `toFun'`	—	`mdifferentiableWithinAt_totalSpace_iff` `coe_mem_source`
`mdifferentiableWithinAt_snd_comp_iff₂` 📖	mathematical	`Bundle.TotalSpace` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `toOpenPartialHomeomorph` `Bundle.TotalSpace.proj` `MDifferentiableWithinAt`	`modelWithCornersSelf` `chartedSpaceSelf` `toFun'`	—	`MDifferentiableWithinAt.change_section_trivialization`
`mdifferentiableWithinAt_totalSpace_iff` 📖	mathematical	`Bundle.TotalSpace` `Set` `Set.instMembership` `PartialEquiv.source` `OpenPartialHomeomorph.toPartialEquiv` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `toOpenPartialHomeomorph` `Bundle.TotalSpace.proj`	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `modelWithCornersSelf` `FiberBundle.chartedSpace` `chartedSpaceSelf` `toFun'`	—	`mdifferentiableWithinAt_totalSpace` `mdifferentiableWithinAt_snd_comp_iff₂` `instMemTrivializationAtlasTrivializationAt` `FiberBundle.mem_trivializationAt_proj_source`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mDifferentiableOn_sub_section` 📖	mathematical	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`mdifferentiableWithinAt_sub_section`
`mdifferentiableAt_add_section` 📖	mathematical	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`mdifferentiableWithinAt_univ` `mdifferentiableWithinAt_add_section`
`mdifferentiableAt_coordChangeL` 📖	mathematical	`Set` `Set.instMembership` `Trivialization.baseSet` `Bundle.TotalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Bundle.TotalSpace.proj`	`MDifferentiableAt` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `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` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Trivialization.coordChangeL` `trivialization_linear`	—	`ContMDiffAt.mdifferentiableAt` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `trivialization_linear` `contMDiffAt_coordChangeL` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero`
`mdifferentiableAt_neg_section` 📖	mathematical	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`mdifferentiableWithinAt_univ` `mdifferentiableWithinAt_neg_section`
`mdifferentiableAt_section` 📖	mathematical	—	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `chartedSpaceSelf` `Trivialization.toFun'` `Bundle.TotalSpace.proj` `FiberBundle.trivializationAt`	—	`mdifferentiableWithinAt_section`
`mdifferentiableAt_sub_section` 📖	mathematical	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg` `mdifferentiableAt_add_section` `mdifferentiableAt_neg_section`
`mdifferentiableAt_totalSpace` 📖	mathematical	—	`MDifferentiableAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.proj` `chartedSpaceSelf` `Trivialization.toFun'` `FiberBundle.trivializationAt`	—	`mdifferentiableWithinAt_totalSpace`
`mdifferentiableOn_add_section` 📖	mathematical	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`mdifferentiableWithinAt_add_section`
`mdifferentiableOn_coordChangeL` 📖	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.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` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `Trivialization.coordChangeL` `trivialization_linear` `Set` `Set.instInter` `Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`ContMDiffOn.mdifferentiableOn` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `trivialization_linear` `contMDiffOn_coordChangeL` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero`
`mdifferentiableOn_neg_section` 📖	mathematical	`MDifferentiableOn` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`mdifferentiableWithinAt_neg_section`
`mdifferentiableOn_symm_coordChangeL` 📖	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.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` `ContinuousLinearEquiv.toContinuousLinearMap` `RingHomInvPair.ids` `ContinuousLinearEquiv.symm` `Trivialization.coordChangeL` `trivialization_linear` `Set` `Set.instInter` `Trivialization.baseSet` `Bundle.TotalSpace` `Bundle.TotalSpace.proj`	—	`ContMDiffOn.mdifferentiableOn` `RingHomIsometric.ids` `smulCommClass_self` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `RingHomInvPair.ids` `trivialization_linear` `contMDiffOn_symm_coordChangeL` `one_ne_zero` `NeZero.charZero_one` `WithTop.charZero`
`mdifferentiableWithinAt_add_section` 📖	mathematical	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`mdifferentiableWithinAt_section` `MDifferentiableWithinAt.congr_of_eventuallyEq` `MDifferentiableWithinAt.add` `Filter.eventually_of_mem` `mem_nhdsWithin_of_mem_nhds` `IsOpen.mem_nhds` `Trivialization.open_baseSet` `FiberBundle.mem_baseSet_trivializationAt` `IsLinearMap.map_add` `Trivialization.linear` `trivialization_linear` `instMemTrivializationAtlasTrivializationAt` `FiberBundle.mem_baseSet_trivializationAt'`
`mdifferentiableWithinAt_neg_section` 📖	mathematical	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`mdifferentiableWithinAt_section` `MDifferentiableWithinAt.congr_of_eventuallyEq` `MDifferentiableWithinAt.neg` `Filter.eventually_of_mem` `mem_nhdsWithin_of_mem_nhds` `IsOpen.mem_nhds` `Trivialization.open_baseSet` `FiberBundle.mem_baseSet_trivializationAt` `IsLinearMap.map_neg` `Trivialization.linear` `trivialization_linear` `instMemTrivializationAtlasTrivializationAt` `FiberBundle.mem_baseSet_trivializationAt'`
`mdifferentiableWithinAt_section` 📖	mathematical	—	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'` `chartedSpaceSelf` `Trivialization.toFun'` `Bundle.TotalSpace.proj` `FiberBundle.trivializationAt`	—	`mdifferentiableWithinAt_totalSpace`
`mdifferentiableWithinAt_smul_const_section` 📖	mathematical	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`MDifferentiableWithinAt.smul_section` `mdifferentiableWithinAt_const`
`mdifferentiableWithinAt_sub_section` 📖	mathematical	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`sub_eq_add_neg` `mdifferentiableWithinAt_add_section` `mdifferentiableWithinAt_neg_section`
`mdifferentiableWithinAt_totalSpace` 📖	mathematical	—	`MDifferentiableWithinAt` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.proj` `chartedSpaceSelf` `Trivialization.toFun'` `FiberBundle.trivializationAt`	—	`FiberBundle.continuousWithinAt_totalSpace` `modelWithCornersSelf_prod` `FiberBundle.extChartAt` `mdifferentiableWithinAt_prod_iff` `ContinuousWithinAt.comp` `Continuous.continuousWithinAt` `FiberBundle.continuous_proj` `Set.mapsTo_image` `IsOpen.mem_nhds` `Trivialization.open_baseSet` `FiberBundle.mem_baseSet_trivializationAt` `Filter.EventuallyEq.mdifferentiableWithinAt_iff` `Filter.eventually_of_mem` `Trivialization.coe_fst'` `Trivialization.coe_fst`
`mdifferentiable_add_section` 📖	mathematical	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Pi.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `AddCommGroup.toAddCommMonoid`	—	`mdifferentiableAt_add_section`
`mdifferentiable_neg_section` 📖	mathematical	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`mdifferentiableAt_neg_section`
`mdifferentiable_smul_const_section` 📖	mathematical	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`MDifferentiableAt.smul_const_section`
`mdifferentiable_smul_section` 📖	mathematical	`MDifferentiable` `NonUnitalNormedRing.toNormedAddCommGroup` `NonUnitalNormedCommRing.toNonUnitalNormedRing` `NormedCommRing.toNonUnitalNormedCommRing` `NormedField.toNormedCommRing` `NontriviallyNormedField.toNormedField` `NormedField.toNormedSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `modelWithCornersSelf` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `chartedSpaceSelf` `Prod.normedAddCommGroup` `Prod.normedSpace` `ModelProd` `instTopologicalSpaceModelProd` `ModelWithCorners.prod` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid`	—	`MDifferentiableAt.smul_section`
`mdifferentiable_sub_section` 📖	mathematical	`MDifferentiable` `Prod.normedAddCommGroup` `Prod.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `ModelProd` `instTopologicalSpaceModelProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ModelWithCorners.prod` `modelWithCornersSelf` `Bundle.TotalSpace` `FiberBundle.chartedSpace` `Bundle.TotalSpace.mk'`	`Pi.instSub` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup`	—	`mdifferentiableAt_sub_section`

---

← Back to Index