Riemannian

📁 Source: Mathlib/Topology/VectorBundle/Riemannian.lean

Statistics

Metric	Count
Definitions ContinuousRiemannianMetric, inner, toRiemannianMetric, RiemannianBundle, g, RiemannianMetric, inner, toCore, instInnerProductSpaceReal, instNormedAddCommGroupOfRiemannianBundle, IsContinuousRiemannianBundle	11
Theorems continuous, isVonNBounded, pos, continuousAt, isVonNBounded, pos, instIsContinuousRiemannianBundle, inner_bundle, inner_bundle, inner_bundle, inner_bundle, exists_continuous, eventually_norm_symmL_trivializationAt_comp_self_lt, eventually_norm_symmL_trivializationAt_lt, eventually_norm_symmL_trivializationAt_self_comp_lt, eventually_norm_trivializationAt_lt, instIsContinuousRiemannianBundleTrivial	17
Total	28

Bundle

Definitions

Name	Category	Theorems
ContinuousRiemannianMetric 📖	CompData	—
RiemannianBundle 📖	CompData	—
RiemannianMetric 📖	CompData	—
instInnerProductSpaceReal 📖	CompOp	7 math math: eventually_enorm_mfderivWithin_symm_extChartAt_lt, instIsContinuousRiemannianBundle, eventually_norm_mfderivWithin_symm_extChartAt_lt, instIsContMDiffRiemannianBundle, eventually_enorm_mfderiv_extChartAt_lt, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, eventually_norm_mfderiv_extChartAt_lt
instNormedAddCommGroupOfRiemannianBundle 📖	CompOp	18 math math: setOf_riemmanianEDist_lt_subset_nhds, eventually_enorm_mfderivWithin_symm_extChartAt_lt, instIsContinuousRiemannianBundle, eventually_norm_mfderivWithin_symm_extChartAt_lt, eventually_riemmanianEDist_lt, instIsContMDiffRiemannianBundle, eventually_enorm_mfderiv_extChartAt_lt, enorm_tangentSpace_vectorSpace, setOf_riemannianEDist_lt_subset_nhds, eventually_riemannianEDist_le_edist_extChartAt, norm_tangentSpace_vectorSpace, eventually_norm_mfderivWithin_symm_extChartAt_comp_lt, setOf_riemmanianEDist_lt_subset_nhds', nnnorm_tangentSpace_vectorSpace, IsRiemannianManifold.out, eventually_norm_mfderiv_extChartAt_lt, setOf_riemannianEDist_lt_subset_nhds', eventually_riemannianEDist_lt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsContinuousRiemannianBundle 📖	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	IsContinuousRiemannianBundle instNormedAddCommGroupOfRiemannianBundle ContinuousRiemannianMetric.toRiemannianMetric instInnerProductSpaceReal	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul RingHomIsometric.ids Trivial.vectorBundle ContinuousMul.to_continuousSMul ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids ContinuousRiemannianMetric.continuous

Bundle.ContinuousRiemannianMetric

Definitions

Name	Category	Theorems
inner 📖	CompOp	4 math math: symm, continuous, pos, isVonNBounded
toRiemannianMetric 📖	CompOp	1 math math: Bundle.instIsContinuousRiemannianBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous 📖	mathematical	—	Continuous Bundle.TotalSpace ContinuousLinearMap Real 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 AddCommGroup.toAddCommMonoid Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField ContinuousLinearMap.toNormedAddCommGroup Real.normedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing ContinuousLinearMap.toNormedSpace NontriviallyNormedField.toNormedField ContinuousLinearMap.addCommGroup Real.instAddCommGroup Bundle.Trivial.topologicalSpace Bundle.Trivial.fiberBundle Bundle.Trivial.vectorBundle ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace NormedField.toNormedCommRing MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Bundle.ContinuousLinearMap.fiberBundle Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids 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	—	—

Bundle.RiemannianBundle

Definitions

Name	Category	Theorems
g 📖	CompOp	—

Bundle.RiemannianMetric

Definitions

Name	Category	Theorems
inner 📖	CompOp	4 math math: isVonNBounded, symm, pos, continuousAt
toCore 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt 📖	mathematical	—	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DFunLike.coe ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid 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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
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	—	—

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	Continuous Bundle.TotalSpace	Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	ContinuousAt.inner_bundle

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	ContinuousAt Bundle.TotalSpace	Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	ContinuousWithinAt.inner_bundle

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	ContinuousOn Bundle.TotalSpace	Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	ContinuousWithinAt.inner_bundle

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inner_bundle 📖	mathematical	ContinuousWithinAt Bundle.TotalSpace	Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Inner.inner InnerProductSpace.toInner Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup	—	instIsTopologicalAddGroupReal IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal IsTopologicalSemiring.toContinuousMul RingHomIsometric.ids Bundle.Trivial.vectorBundle ContinuousMul.to_continuousSMul Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids IsContinuousRiemannianBundle.exists_continuous clm_bundle_apply₂ ContinuousAt.comp_continuousWithinAt Continuous.continuousAt

IsContinuousRiemannianBundle

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_continuous 📖	mathematical	—	Continuous Bundle.TotalSpace ContinuousLinearMap Real 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 Bundle.ContinuousLinearMap.topologicalSpaceTotalSpace DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField NormedAddCommGroup.toAddCommGroup ContinuousLinearMap.toNormedAddCommGroup Real.normedAddCommGroup RingHomIsometric.ids SeminormedCommRing.toSeminormedRing ContinuousLinearMap.toNormedSpace NontriviallyNormedField.toNormedField ContinuousLinearMap.addCommGroup Real.instAddCommGroup Bundle.Trivial.topologicalSpace Bundle.Trivial.fiberBundle Bundle.Trivial.vectorBundle ContinuousMul.to_continuousSMul SeminormedRing.toPseudoMetricSpace NormedField.toNormedCommRing MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Bundle.ContinuousLinearMap.fiberBundle Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids Bundle.TotalSpace.mk' Inner.inner InnerProductSpace.toInner DFunLike.coe ContinuousLinearMap.funLike	—	—

(root)

Definitions

Name	Category	Theorems
IsContinuousRiemannianBundle 📖	CompData	2 math math: Bundle.instIsContinuousRiemannianBundle, instIsContinuousRiemannianBundleTrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eventually_norm_symmL_trivializationAt_comp_self_lt 📖	mathematical	Real Real.instLT Real.instOne	Filter.Eventually Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike ContinuousLinearMap.hasOpNorm ContinuousLinearMap.comp RingHomCompTriple.ids Trivialization.symmL FiberBundle.trivializationAt trivialization_linear instMemTrivializationAtlasTrivializationAt Trivialization.continuousLinearMapAt nhds	—	RingHomCompTriple.ids trivialization_linear instMemTrivializationAtlasTrivializationAt exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing FiberBundle.mem_baseSet_trivializationAt' RingHomInvPair.ids self_mem_nhdsWithin Filter.tendsto_inf_left Filter.Tendsto.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal tendsto_const_nhds Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul Filter.tendsto_id tendsto_order instOrderTopologyReal MulZeroClass.zero_mul add_zero LT.lt.trans_le le_abs_self Filter.Eventually.exists nhdsGT_neBot instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.Eventually.and instIsTopologicalAddGroupReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal RingHomIsometric.ids Bundle.Trivial.vectorBundle ContinuousMul.to_continuousSMul Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids IsContinuousRiemannianBundle.exists_continuous Continuous.continuousAt SeminormedAddCommGroup.toIsTopologicalAddGroup Metric.continuousAt_iff' Filter.mp_mem IsOpen.mem_nhds Trivialization.open_baseSet Filter.univ_mem' dist_eq_norm LT.lt.le LE.le.trans_lt ContinuousLinearMap.opNorm_le_bound le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_neg_of_lt IsTopologicalAddGroup.toContinuousAdd smulCommClass_self ContinuousSMul.continuousConstSMul inCoordinates_apply_eq₂ Set.mem_univ Trivialization.coe_continuousLinearEquivAt_eq ContinuousLinearEquiv.symm_apply_apply Bundle.Trivial.linearMapAt_trivialization sub_add_cancel le_imp_le_of_le_of_le IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul le_refl add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ContinuousLinearMap.le_opNorm₂ Real.le_norm_self pow_two mul_assoc mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono mul_nonneg IsOrderedRing.toPosMulMono norm_nonneg mul_le_mul_of_nonneg_left pow_le_pow_left₀ ContinuousLinearMap.le_opNorm le_of_lt ContinuousLinearEquiv.apply_symm_apply Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero inner_self_eq_norm_sq_to_K Mathlib.Tactic.Ring.add_pf_add_gt real_inner_self_eq_norm_sq Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul le_of_sq_le_sq mul_pow lt_trans Mathlib.Meta.Positivity.pos_of_isNat
eventually_norm_symmL_trivializationAt_lt 📖	mathematical	—	Real Real.instLT Real.instZero Filter.Eventually Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike ContinuousLinearMap.hasOpNorm Trivialization.symmL FiberBundle.trivializationAt trivialization_linear instMemTrivializationAtlasTrivializationAt nhds	—	trivialization_linear instMemTrivializationAtlasTrivializationAt Nat.instAtLeastTwoHAddOfNat mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_one norm_nonneg RingHomIsometric.ids Filter.mp_mem RingHomCompTriple.ids eventually_norm_symmL_trivializationAt_comp_self_lt one_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Filter.univ_mem' ContinuousLinearMap.ext FiberBundle.mem_baseSet_trivializationAt' RingHomInvPair.ids Trivialization.coe_continuousLinearEquivAt_eq ContinuousLinearEquiv.apply_symm_apply ContinuousLinearMap.comp_id ContinuousLinearMap.comp_assoc lt_imp_lt_of_le_of_le ContinuousLinearMap.opNorm_comp_le le_refl mul_lt_mul'' IsOrderedRing.toMulPosMono lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le
eventually_norm_symmL_trivializationAt_self_comp_lt 📖	mathematical	Real Real.instLT Real.instOne	Filter.Eventually Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike ContinuousLinearMap.hasOpNorm ContinuousLinearMap.comp RingHomCompTriple.ids Trivialization.symmL FiberBundle.trivializationAt trivialization_linear instMemTrivializationAtlasTrivializationAt Trivialization.continuousLinearMapAt nhds	—	RingHomCompTriple.ids trivialization_linear instMemTrivializationAtlasTrivializationAt exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing FiberBundle.mem_baseSet_trivializationAt' RingHomInvPair.ids self_mem_nhdsWithin Filter.tendsto_inf_left Filter.Tendsto.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal tendsto_const_nhds Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.tendsto_id tendsto_order instOrderTopologyReal MulZeroClass.zero_mul sub_zero inv_lt_one_of_one_lt₀ Real.instZeroLEOneClass lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_nonpos_of_le mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Filter.Eventually.exists nhdsGT_neBot instNoMaxOrderOfNontrivial Real.instNontrivial Filter.Eventually.and IsTopologicalSemiring.toContinuousAdd Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul instIsUniformAddGroupReal RingHomIsometric.ids Bundle.Trivial.vectorBundle ContinuousMul.to_continuousSMul Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids IsContinuousRiemannianBundle.exists_continuous Continuous.continuousAt SeminormedAddCommGroup.toIsTopologicalAddGroup Metric.continuousAt_iff' Filter.mp_mem IsOpen.mem_nhds Trivialization.open_baseSet Filter.univ_mem' dist_eq_norm' LT.lt.le LE.le.trans_lt ContinuousLinearMap.opNorm_le_bound le_of_not_gt Mathlib.Tactic.Ring.neg_congr neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one IsTopologicalAddGroup.toContinuousAdd smulCommClass_self ContinuousSMul.continuousConstSMul inCoordinates_apply_eq₂ Set.mem_univ Trivialization.coe_continuousLinearEquivAt_eq ContinuousLinearEquiv.symm_apply_apply Bundle.Trivial.linearMapAt_trivialization sub_add_cancel le_imp_le_of_le_of_le IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul le_refl add_le_add_left ContinuousLinearMap.le_opNorm₂ Real.le_norm_self pow_two mul_assoc mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono mul_nonneg IsOrderedRing.toPosMulMono norm_nonneg mul_le_mul_of_nonneg_left pow_le_pow_left₀ ContinuousLinearMap.le_opNorm le_of_lt ContinuousLinearEquiv.apply_symm_apply inner_self_eq_norm_sq_to_K Mathlib.Tactic.Linarith.add_lt_of_le_of_neg div_eq_inv_mul le_div_iff₀' lt_of_le_of_lt inv_pos_of_pos pow_pos IsStrictOrderedRing.toZeroLEOneClass lt_trans Mathlib.Meta.Positivity.pos_of_isNat inv_le_of_inv_le₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE real_inner_self_eq_norm_sq Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing even_two_mul le_of_sq_le_sq mul_pow
eventually_norm_trivializationAt_lt 📖	mathematical	—	Real Real.instLT Real.instZero Filter.Eventually Norm.norm ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField InnerProductSpace.toNormedSpace Real.instRCLike ContinuousLinearMap.hasOpNorm Trivialization.continuousLinearMapAt FiberBundle.trivializationAt trivialization_linear instMemTrivializationAtlasTrivializationAt nhds	—	trivialization_linear instMemTrivializationAtlasTrivializationAt Nat.instAtLeastTwoHAddOfNat mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one norm_nonneg RingHomIsometric.ids Mathlib.Meta.NormNum.instAtLeastTwo Filter.mp_mem RingHomCompTriple.ids eventually_norm_symmL_trivializationAt_self_comp_lt one_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Filter.univ_mem' ContinuousLinearMap.ext FiberBundle.mem_baseSet_trivializationAt' RingHomInvPair.ids Trivialization.coe_continuousLinearEquivAt_eq ContinuousLinearEquiv.apply_symm_apply ContinuousLinearMap.id_comp ContinuousLinearMap.comp_assoc lt_imp_lt_of_le_of_le ContinuousLinearMap.opNorm_comp_le le_refl mul_lt_mul'' IsOrderedRing.toMulPosMono lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le
instIsContinuousRiemannianBundleTrivial 📖	mathematical	—	IsContinuousRiemannianBundle 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 ContinuousMul.to_continuousSMul Bundle.ContinuousLinearMap.vectorBundle ContinuousLinearMap.topologicalAddGroup ContinuousLinearMap.continuousSMul RingHomSurjective.ids continuous_iff_continuousAt SeminormedAddCommGroup.to_isUniformAddGroup FiberBundle.continuousAt_totalSpace continuousAt_id SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing 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 continuousAt_const

---

← Back to Index