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 instNormedAddCommGroupOfRiemannianBundle ContMDiffRiemannianMetric.toRiemannianMetric instInnerProductSpaceReal	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul RingHomIsometric.ids ContinuousLinearMap.smulCommClass Trivial.vectorBundle IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology 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 SeminormedAddCommGroup.toAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Prod.normedAddCommGroup ContinuousLinearMap.toNormedAddCommGroup Real.normedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing ContinuousLinearMap.toNormedSpace NontriviallyNormedField.toNormedField Prod.normedSpace ContinuousLinearMap.toSeminormedAddCommGroup ContinuousLinearMap.smulCommClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace ContinuousLinearMap.addCommGroup Real.instAddCommGroup Bundle.Trivial.topologicalSpace Bundle.Trivial.fiberBundle Bundle.Trivial.vectorBundle IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace NormedField.toNormedCommRing Real.instAdd SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup IsTopologicalSemiring.toIsModuleTopology 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 SeminormedAddCommGroup.toAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul AddCommMonoid.toAddMonoid MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing 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 SeminormedAddCommGroup.toAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing 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	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace 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	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal 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	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal 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	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace chartedSpaceSelf Inner.inner InnerProductSpace.toInner	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul RingHomIsometric.ids ContinuousLinearMap.smulCommClass Bundle.Trivial.vectorBundle IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology 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 SeminormedAddCommGroup.toAddCommGroup instIsTopologicalAddGroupReal ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousLinearMap.module Algebra.to_smulCommClass Real.instCommSemiring CommSemiring.toSemiring Algebra.id UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Ring.uniformContinuousConstSMul Real.instRing instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Prod.normedAddCommGroup ContinuousLinearMap.toNormedAddCommGroup Real.normedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing ContinuousLinearMap.toNormedSpace NontriviallyNormedField.toNormedField Prod.normedSpace ContinuousLinearMap.toSeminormedAddCommGroup ContinuousLinearMap.smulCommClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField AddCommGroup.toAddCommMonoid ModelProd instTopologicalSpaceModelProd ModelWithCorners.prod modelWithCornersSelf Bundle.TotalSpace Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.addCommGroup Real.instAddCommGroup Bundle.Trivial.topologicalSpace Bundle.Trivial.fiberBundle Bundle.Trivial.vectorBundle IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace NormedField.toNormedCommRing Real.instAdd SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup IsTopologicalSemiring.toIsModuleTopology 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 PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompletelyDistribLattice.toCompleteLattice CompleteLinearOrder.toCompletelyDistribLattice instCompleteLinearOrderENat	IsContMDiffRiemannianBundle	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul RingHomIsometric.ids ContinuousLinearMap.smulCommClass Bundle.Trivial.vectorBundle IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology 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	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace 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	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace 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	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace 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	Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal Real.pseudoMetricSpace chartedSpaceSelf Inner.inner InnerProductSpace.toInner	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul RingHomIsometric.ids ContinuousLinearMap.smulCommClass Bundle.Trivial.vectorBundle IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology 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 instZeroENat	—	IsContMDiffRiemannianBundle.of_le zero_le_one WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass
instIsContMDiffRiemannianBundleOfNatWithTopENat_1 📖	mathematical	—	IsContMDiffRiemannianBundle WithTop ENat WithTop.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat	—	Nat.instAtLeastTwoHAddOfNat IsContMDiffRiemannianBundle.of_le one_le_two WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid
instIsContMDiffRiemannianBundleOfNatWithTopENat_2 📖	mathematical	—	IsContMDiffRiemannianBundle WithTop ENat instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithTop.addMonoidWithOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring instCommSemiringENat Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat IsContMDiffRiemannianBundle.of_le WithTop.addLeftMono IsOrderedAddMonoid.toAddLeftMono LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid WithTop.zeroLEOneClass IsOrderedRing.toZeroLEOneClass 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 IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul RingHomIsometric.ids ContinuousLinearMap.smulCommClass IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.to_isUniformAddGroup ContinuousLinearMap.ext ContinuousLinearMap.comp.congr_simp Bundle.Trivial.symmL_trivialization ContinuousLinearMap.comp_id Trivialization.linearMapAt_apply Set.inter_self Bundle.Trivial.continuousLinearMapAt_trivialization ContinuousLinearMap.id_comp contMDiffAt_const

---

← Back to Index