Structures · Geometry
IsContMDiffRiemannianBundle
Consider a real vector bundle in which each fiber is endowed with a scalar product.
We say that the bundle is Riemannian if the scalar product depends smoothly on the base point.
This assumption is spelled IsContMDiffRiemannianBundle IB n F E where IB is the model space of
the base, n is the smoothness, F is the model fiber, and E : B → Type* is the bundle.
- Shape
- 4 explicit arguments · adds exists_contMDiff
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by22
- CovariantDerivative.derivMetricTensor
- IsContMDiffRiemannianBundle.exists_contMDiff
- ContMDiffWithinAt.inner_bundle
- CovariantDerivative.IsMetricCompatible
- MDifferentiableWithinAt.inner_bundle
- CovariantDerivative.derivMetricTensor_apply
- CovariantDerivative.IsMetricCompatible.mvfderiv_inner_eq
- ContMDiffAt.inner_bundle
- MDifferentiableAt.inner_bundle
- ContMDiff.inner_bundle
- instIsContMDiffRiemannianBundleOfNatWithTopENat
- instIsContMDiffRiemannianBundleOfNatWithTopENat_1
- instIsContMDiffRiemannianBundleOfNatWithTopENat_2
- CovariantDerivative.derivMetricTensor_apply_eq_extend
- IsContMDiffRiemannianBundle.of_le
- CovariantDerivative.isMetricCompatible_iff
- CovariantDerivative.derivMetricTensor.congr_simp
- MDifferentiable.inner_bundle
- MDifferentiableOn.inner_bundle
- ContMDiffOn.inner_bundle
- instIsContMDiffRiemannianBundleOfTopWithTopENat
- instIsContMDiffRiemannianBundleOfSomeENatTopOfLEInfty
Ancestors0
No ancestors.