SmoothSection

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

Statistics

Metric	Count
Definitions ContMDiffSection, coeAddHom, inhabited, instAdd, instAddCommGroup, instDFunLike, instModule, instNSMul, instNeg, instSMul, instSub, instZSMul, instZero, toFun, «termCₛ^_⟮_;_,_⟯»	15
Theorems add_section, const_smul_section, finsum_section_of_locallyFinite, neg_section, smul_section, sub_section, sum_section, sum_section_of_locallyFinite, add_section, const_smul_section, finsum_section_of_locallyFinite, neg_section, smul_section, sub_section, sum_section, sum_section_of_locallyFinite, add_section, const_smul_section, finsum_section_of_locallyFinite, neg_section, smul_section, smul_section_of_tsupport, sub_section, sum_section, sum_section_of_locallyFinite, coeAddHom_apply, coeFn_mk, coe_add, coe_inj, coe_injective, coe_neg, coe_nsmul, coe_smul, coe_sub, coe_zero, coe_zsmul, contMDiff, contMDiff_toFun, ext, ext_iff, mdifferentiable, mdifferentiable', mdifferentiableAt, add_section, const_smul_section, finsum_section_of_locallyFinite, neg_section, smul_section, sub_section, sum_section, sum_section_of_locallyFinite	51
Total	66

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_section 📖	mathematical	ContMDiff 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	—	ContMDiffAt.add_section
const_smul_section 📖	mathematical	ContMDiff 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	—	ContMDiffAt.const_smul_section
finsum_section_of_locallyFinite 📖	mathematical	LocallyFinite setOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContMDiff 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	—	ContMDiffAt.finsum_section_of_locallyFinite
neg_section 📖	mathematical	ContMDiff 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	—	ContMDiffAt.neg_section
smul_section 📖	mathematical	ContMDiff 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	—	ContMDiffAt.smul_section
sub_section 📖	mathematical	ContMDiff 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	—	ContMDiffAt.sub_section
sum_section 📖	mathematical	ContMDiff 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	—	ContMDiffAt.sum_section
sum_section_of_locallyFinite 📖	mathematical	LocallyFinite setOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContMDiff 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	—	ContMDiffAt.sum_section_of_locallyFinite

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_section 📖	mathematical	ContMDiffAt 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	—	contMDiffWithinAt_univ ContMDiffWithinAt.add_section
const_smul_section 📖	mathematical	ContMDiffAt 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 contMDiffAt_const
finsum_section_of_locallyFinite 📖	mathematical	LocallyFinite setOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContMDiffAt 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	—	ContMDiffWithinAt.finsum_section_of_locallyFinite
neg_section 📖	mathematical	ContMDiffAt 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	—	contMDiffWithinAt_univ ContMDiffWithinAt.neg_section
smul_section 📖	mathematical	ContMDiffAt 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	—	contMDiffWithinAt_univ ContMDiffWithinAt.smul_section
sub_section 📖	mathematical	ContMDiffAt 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 add_section neg_section
sum_section 📖	mathematical	ContMDiffAt 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	—	ContMDiffWithinAt.sum_section
sum_section_of_locallyFinite 📖	mathematical	LocallyFinite setOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContMDiffAt 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	—	ContMDiffWithinAt.sum_section_of_locallyFinite

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_section 📖	mathematical	ContMDiffOn 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	—	ContMDiffWithinAt.add_section
const_smul_section 📖	mathematical	ContMDiffOn 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 contMDiffOn_const
finsum_section_of_locallyFinite 📖	mathematical	LocallyFinite setOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContMDiffOn 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	—	ContMDiffWithinAt.finsum_section_of_locallyFinite
neg_section 📖	mathematical	ContMDiffOn 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	—	ContMDiffWithinAt.neg_section
smul_section 📖	mathematical	ContMDiffOn 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	—	ContMDiffWithinAt.smul_section
smul_section_of_tsupport 📖	mathematical	ContMDiffOn 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'	ContMDiff 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	—	contMDiff_of_contMDiffOn_union_of_isOpen smul_section congr ContMDiff.contMDiffOn Bundle.contMDiff_zeroSection image_eq_zero_of_notMem_tsupport zero_smul Set.compl_subset_iff_union Set.compl_subset_compl isOpen_compl_iff isClosed_tsupport
sub_section 📖	mathematical	ContMDiffOn 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	—	ContMDiffWithinAt.sub_section
sum_section 📖	mathematical	ContMDiffOn 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	—	ContMDiffWithinAt.sum_section
sum_section_of_locallyFinite 📖	mathematical	LocallyFinite setOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContMDiffOn 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	—	ContMDiffWithinAt.sum_section_of_locallyFinite

ContMDiffSection

Definitions

Name	Category	Theorems
coeAddHom 📖	CompOp	1 math math: coeAddHom_apply
inhabited 📖	CompOp	—
instAdd 📖	CompOp	1 math math: coe_add
instAddCommGroup 📖	CompOp	1 math math: coeAddHom_apply
instDFunLike 📖	CompOp	18 math math: coe_injective, coe_nsmul, exists_contMDiffSection_forall_mem_convex_of_local, coe_zero, coe_smul, coe_sub, coe_add, coeAddHom_apply, exists_smooth_section_forall_mem_convex_of_local, exists_contMDiffOn_section_forall_mem_convex_of_local, contMDiff, ext_iff, mdifferentiable', mdifferentiableAt, mdifferentiable, coe_neg, coe_zsmul, coeFn_mk
instModule 📖	CompOp	—
instNSMul 📖	CompOp	1 math math: coe_nsmul
instNeg 📖	CompOp	1 math math: coe_neg
instSMul 📖	CompOp	1 math math: coe_smul
instSub 📖	CompOp	1 math math: coe_sub
instZSMul 📖	CompOp	1 math math: coe_zsmul
instZero 📖	CompOp	1 math math: coe_zero
toFun 📖	CompOp	1 math math: contMDiff_toFun

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeAddHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom ContMDiffSection AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroup Pi.addZeroClass AddMonoidHom.instFunLike coeAddHom instDFunLike	—	—
coeFn_mk 📖	mathematical	ContMDiff Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace	DFunLike.coe ContMDiffSection instDFunLike	—	—
coe_add 📖	mathematical	—	DFunLike.coe ContMDiffSection instDFunLike instAdd Pi.instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	—
coe_inj 📖	—	DFunLike.coe ContMDiffSection instDFunLike	—	—	DFunLike.ext'
coe_injective 📖	mathematical	—	ContMDiffSection DFunLike.coe instDFunLike	—	—
coe_neg 📖	mathematical	—	DFunLike.coe ContMDiffSection instDFunLike instNeg Pi.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_nsmul 📖	mathematical	—	DFunLike.coe ContMDiffSection instDFunLike instNSMul AddMonoid.toNatSMul Pi.addMonoid SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	zero_smul succ_nsmul
coe_smul 📖	mathematical	—	DFunLike.coe ContMDiffSection instDFunLike instSMul Pi.instSMul SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	—
coe_sub 📖	mathematical	—	DFunLike.coe ContMDiffSection instDFunLike instSub Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	—
coe_zero 📖	mathematical	—	DFunLike.coe ContMDiffSection instDFunLike instZero Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
coe_zsmul 📖	mathematical	—	DFunLike.coe ContMDiffSection instDFunLike instZSMul SubNegMonoid.toZSMul Pi.subNegMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	coe_nsmul natCast_zsmul negSucc_zsmul
contMDiff 📖	mathematical	—	ContMDiff 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' DFunLike.coe ContMDiffSection instDFunLike	—	contMDiff_toFun
contMDiff_toFun 📖	mathematical	—	ContMDiff 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' toFun	—	—
ext 📖	—	DFunLike.coe ContMDiffSection instDFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe ContMDiffSection instDFunLike	—	ext
mdifferentiable 📖	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' DFunLike.coe ContMDiffSection WithTop.some ENat Top.top instTopENat instDFunLike	—	ContMDiff.mdifferentiable contMDiff
mdifferentiable' 📖	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' DFunLike.coe ContMDiffSection instDFunLike	—	ContMDiff.mdifferentiable contMDiff
mdifferentiableAt 📖	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' DFunLike.coe ContMDiffSection WithTop.some ENat Top.top instTopENat instDFunLike	—	mdifferentiable

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_section 📖	mathematical	ContMDiffWithinAt 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	—	Bundle.contMDiffWithinAt_section congr_of_eventuallyEq add instContMDiffAddSelf 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'
const_smul_section 📖	mathematical	ContMDiffWithinAt 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 contMDiffWithinAt_const
finsum_section_of_locallyFinite 📖	mathematical	LocallyFinite setOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContMDiffWithinAt 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 tsum_eq_finsum SummationFilter.instLeAtTopUnconditional Set.mem_setOf mem_of_mem_nhds Set.Finite.subset
neg_section 📖	mathematical	ContMDiffWithinAt 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	—	Bundle.contMDiffWithinAt_section congr_of_eventuallyEq neg instNormedSpaceLieAddGroup 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'
smul_section 📖	mathematical	ContMDiffWithinAt 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	—	Bundle.contMDiffWithinAt_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'
sub_section 📖	mathematical	ContMDiffWithinAt 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 add_section neg_section
sum_section 📖	mathematical	ContMDiffWithinAt 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 Bundle.contMDiffWithinAt_zeroSection Finset.sum_insert add_section Finset.mem_insert_self Finset.mem_insert_of_mem
sum_section_of_locallyFinite 📖	mathematical	LocallyFinite setOf NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid ContMDiffWithinAt 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 contMDiffWithinAt_inter congr tsum_eq_sum' SummationFilter.instLeAtTopUnconditional Function.support_subset_iff' Set.mem_toFinset Set.mem_of_mem_inter_right mem_of_mem_nhds

Manifold

Definitions

Name	Category	Theorems
«termCₛ^_⟮_;_,_⟯» 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
ContMDiffSection 📖	CompData	18 math math: ContMDiffSection.coe_injective, ContMDiffSection.coe_nsmul, exists_contMDiffSection_forall_mem_convex_of_local, ContMDiffSection.coe_zero, ContMDiffSection.coe_smul, ContMDiffSection.coe_sub, ContMDiffSection.coe_add, ContMDiffSection.coeAddHom_apply, exists_smooth_section_forall_mem_convex_of_local, exists_contMDiffOn_section_forall_mem_convex_of_local, ContMDiffSection.contMDiff, ContMDiffSection.ext_iff, ContMDiffSection.mdifferentiable', ContMDiffSection.mdifferentiableAt, ContMDiffSection.mdifferentiable, ContMDiffSection.coe_neg, ContMDiffSection.coe_zsmul, ContMDiffSection.coeFn_mk

---

← Back to Index