Riemannian

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

Statistics

Metric	Count
Definitions ContMDiffRiemannianMetric, inner, toContinuousRiemannianMetric, toRiemannianMetric, IsContMDiffRiemannianBundle	5
Theorems contMDiff, isVonNBounded, pos, instIsContMDiffRiemannianBundle, inner_bundle, inner_bundle, inner_bundle, inner_bundle, exists_contMDiff, of_le, inner_bundle, inner_bundle, inner_bundle, inner_bundle, instIsContMDiffRiemannianBundleOfNatWithTopENat, instIsContMDiffRiemannianBundleOfNatWithTopENat_1, instIsContMDiffRiemannianBundleOfNatWithTopENat_2, instIsContMDiffRiemannianBundleOfSomeENatTopOfLEInfty, instIsContMDiffRiemannianBundleOfTopWithTopENat, instIsContMDiffRiemannianBundleTrivial	20
Total	25

Bundle

Definitions

Name	Category	Theorems
ContMDiffRiemannianMetric 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsContMDiffRiemannianBundle 📖	mathematical	IsTopologicalAddGroup AddCommGroup.toAddGroup ContinuousConstSMul Real SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid	IsContMDiffRiemannianBundle instNormedAddCommGroupOfRiemannianBundleOfIsTopologicalAddGroupOfContinuousConstSMulReal ContMDiffRiemannianMetric.toRiemannianMetric instInnerProductSpaceReal	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul RingHomIsometric.ids ContinuousLinearMap.smulCommClass Trivial.vectorBundle IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids ContMDiffRiemannianMetric.contMDiff

Bundle.ContMDiffRiemannianMetric

Definitions

Name	Category	Theorems
inner 📖	CompOp	4 math math: isVonNBounded, contMDiff, symm, pos
toContinuousRiemannianMetric 📖	CompOp	—
toRiemannianMetric 📖	CompOp	1 math math: Bundle.instIsContMDiffRiemannianBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contMDiff 📖	mathematical	—	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal ContinuousLinearMap.topologicalSpace NormedAddCommGroup.toAddCommGroup Real.instAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul Prod.normedAddCommGroup ContinuousLinearMap.toNormedAddCommGroup Real.normedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing ContinuousLinearMap.toNormedSpace NontriviallyNormedField.toNormedField Prod.normedSpace ContinuousLinearMap.toSeminormedAddCommGroup ContinuousLinearMap.smulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Module.toDistribMulAction ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace ContinuousLinearMap.addCommGroup Real.instRing Bundle.Trivial.topologicalSpace Bundle.Trivial.fiberBundle Bundle.Trivial.vectorBundle IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace NormedField.toNormedCommRing Real.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring Bundle.ContinuousLinearMap.fiberBundle Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids FiberBundle.chartedSpace Bundle.TotalSpace.mk' inner	—	—
isVonNBounded 📖	mathematical	—	Bornology.IsVonNBounded Real SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction Real.semiring AddCommGroup.toAddCommMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid setOf Real.instLT DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace Real.instAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul inner Real.instOne	—	—
pos 📖	mathematical	—	Real Real.instLT Real.instZero DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal ContinuousLinearMap.funLike ContinuousLinearMap.topologicalSpace Real.instAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul inner	—	—

ContMDiff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace modelWithCornersSelf chartedSpaceSelf Inner.inner InnerProductSpace.toInner	—	ContMDiffAt.inner_bundle

ContMDiffAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	ContMDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace	ContMDiffAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf Inner.inner InnerProductSpace.toInner	—	ContMDiffWithinAt.inner_bundle

ContMDiffOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	ContMDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace	ContMDiffOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf Inner.inner InnerProductSpace.toInner	—	ContMDiffWithinAt.inner_bundle

ContMDiffWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	ContMDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace	ContMDiffWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace modelWithCornersSelf Real.pseudoMetricSpace chartedSpaceSelf Inner.inner InnerProductSpace.toInner	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul RingHomIsometric.ids ContinuousLinearMap.smulCommClass Bundle.Trivial.vectorBundle IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids IsContMDiffRiemannianBundle.exists_contMDiff clm_bundle_apply₂ ContMDiffAt.comp_contMDiffWithinAt ContMDiff.contMDiffAt

IsContMDiffRiemannianBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_contMDiff 📖	mathematical	—	ContMDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Real.pseudoMetricSpace Real.instAddCommMonoid NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal ContinuousLinearMap.topologicalSpace NormedAddCommGroup.toAddCommGroup Real.instAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsSemitopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id SeparatelyContinuousMul.to_continuousSMul Real.instMul IsSemitopologicalSemiring.toSeparatelyContinuousMul Prod.normedAddCommGroup ContinuousLinearMap.toNormedAddCommGroup Real.normedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing ContinuousLinearMap.toNormedSpace NontriviallyNormedField.toNormedField Prod.normedSpace ContinuousLinearMap.toSeminormedAddCommGroup ContinuousLinearMap.smulCommClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommMonoid.toAddMonoid AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Module.toDistribMulAction ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace ContinuousLinearMap.addCommGroup Real.instRing Bundle.Trivial.topologicalSpace Bundle.Trivial.fiberBundle Bundle.Trivial.vectorBundle IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace NormedField.toNormedCommRing Real.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring Bundle.ContinuousLinearMap.fiberBundle Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids FiberBundle.chartedSpace Bundle.TotalSpace.mk' Inner.inner InnerProductSpace.toInner DFunLike.coe ContinuousLinearMap.funLike	—	—
of_le 📖	mathematical	WithTop ENat Preorder.toLE WithTop.instPreorder instPreorderENat	IsContMDiffRiemannianBundle	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul RingHomIsometric.ids ContinuousLinearMap.smulCommClass Bundle.Trivial.vectorBundle IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids exists_contMDiff ContMDiff.of_le

MDifferentiable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	MDifferentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace	MDifferentiable Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace modelWithCornersSelf chartedSpaceSelf Inner.inner InnerProductSpace.toInner	—	MDifferentiableAt.inner_bundle

MDifferentiableAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	MDifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace	MDifferentiableAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace modelWithCornersSelf chartedSpaceSelf Inner.inner InnerProductSpace.toInner	—	MDifferentiableWithinAt.inner_bundle

MDifferentiableOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	MDifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace	MDifferentiableOn Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace modelWithCornersSelf chartedSpaceSelf Inner.inner InnerProductSpace.toInner	—	MDifferentiableWithinAt.inner_bundle

MDifferentiableWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	MDifferentiableWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Prod.normedAddCommGroup Prod.normedSpace NontriviallyNormedField.toNormedField NormedAddCommGroup.toSeminormedAddCommGroup ModelProd instTopologicalSpaceModelProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace FiberBundle.chartedSpace	MDifferentiableWithinAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace modelWithCornersSelf chartedSpaceSelf Inner.inner InnerProductSpace.toInner	—	instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul RingHomIsometric.ids ContinuousLinearMap.smulCommClass Bundle.Trivial.vectorBundle IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids IsContMDiffRiemannianBundle.exists_contMDiff clm_bundle_apply₂ MDifferentiableAt.comp_mdifferentiableWithinAt ContMDiff.mdifferentiableAt one_ne_zero NeZero.charZero_one WithTop.charZero

(root)

Definitions

Name	Category	Theorems
IsContMDiffRiemannianBundle 📖	CompData	8 math math: instIsContMDiffRiemannianBundleOfTopWithTopENat, instIsContMDiffRiemannianBundleOfNatWithTopENat_1, instIsContMDiffRiemannianBundleOfSomeENatTopOfLEInfty, instIsContMDiffRiemannianBundleOfNatWithTopENat_2, IsContMDiffRiemannianBundle.of_le, Bundle.instIsContMDiffRiemannianBundle, instIsContMDiffRiemannianBundleTrivial, instIsContMDiffRiemannianBundleOfNatWithTopENat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsContMDiffRiemannianBundleOfNatWithTopENat 📖	mathematical	—	IsContMDiffRiemannianBundle WithTop ENat WithTop.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	IsContMDiffRiemannianBundle.of_le zero_le_one WithTop.zeroLEOneClass
instIsContMDiffRiemannianBundleOfNatWithTopENat_1 📖	mathematical	—	IsContMDiffRiemannianBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne instAddMonoidWithOneENat	—	Nat.instAtLeastTwoHAddOfNat IsContMDiffRiemannianBundle.of_le one_le_two WithTop.zeroLEOneClass WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid
instIsContMDiffRiemannianBundleOfNatWithTopENat_2 📖	mathematical	—	IsContMDiffRiemannianBundle WithTop ENat instOfNatAtLeastTwo WithTop.natCast ENat.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat IsContMDiffRiemannianBundle.of_le WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass WithTop.charZero
instIsContMDiffRiemannianBundleOfSomeENatTopOfLEInfty 📖	mathematical	—	IsContMDiffRiemannianBundle	—	IsContMDiffRiemannianBundle.of_le ENat.LEInfty.out
instIsContMDiffRiemannianBundleOfTopWithTopENat 📖	mathematical	—	IsContMDiffRiemannianBundle	—	IsContMDiffRiemannianBundle.of_le le_top
instIsContMDiffRiemannianBundleTrivial 📖	mathematical	—	IsContMDiffRiemannianBundle InnerProductSpace.toNormedSpace Real Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup Bundle.Trivial Bundle.Trivial.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace Bundle.Trivial.fiberBundle Bundle.Trivial.vectorBundle DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField	—	Bundle.Trivial.vectorBundle instIsTopologicalAddGroupReal IsSemitopologicalSemiring.toContinuousAdd IsSemitopologicalRing.toIsSemitopologicalSemiring IsTopologicalRing.toIsSemitopologicalRing instIsTopologicalRingReal Algebra.to_smulCommClass SeparatelyContinuousMul.to_continuousSMul IsSemitopologicalSemiring.toSeparatelyContinuousMul RingHomIsometric.ids ContinuousLinearMap.smulCommClass IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.ext ContinuousLinearMap.comp.congr_simp Bundle.Trivial.symmL_trivialization ContinuousLinearMap.comp_id Bundle.Trivialization.linearMapAt_apply Set.inter_self Bundle.Trivial.continuousLinearMapAt_trivialization ContinuousLinearMap.id_comp contMDiffAt_const

---

← Back to Index