Structures · Topology
IsContinuousRiemannianBundle
Consider a real vector bundle in which each fiber is endowed with an inner product.
We say that the bundle is Riemannian if the inner product depends continuously on the base point.
This assumption is spelled IsContinuousRiemannianBundle F E where F is the model fiber,
and E : B → Type* is the bundle.
- Defined in
- Mathlib.Topology.VectorBundle.Riemannian
- Shape
- 2 explicit arguments · adds exists_continuous
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 by25
- IsContinuousRiemannianBundle.exists_continuous
- ContinuousWithinAt.inner_bundle
- setOfPred_riemannianEDist_lt_subset_nhds
- eventually_enorm_mfderiv_extChartAt_lt
- ContinuousAt.inner_bundle
- eventually_norm_symmL_trivializationAt_comp_self_lt
- eventually_norm_symmL_trivializationAt_lt
- eventually_riemannianEDist_le_edist_extChartAt
- eventually_norm_mfderiv_extChartAt_lt
- eventually_enorm_mfderivWithin_symm_extChartAt_lt
- eventually_norm_mfderivWithin_symm_extChartAt_lt
- eventually_norm_symmL_trivializationAt_self_comp_lt
- eventually_norm_mfderivWithin_symm_extChartAt_comp_lt
- eventually_norm_trivializationAt_lt
- setOfPred_riemannianEDist_lt_subset_nhds'
- setOf_riemannianEDist_lt_subset_nhds
- eventually_riemannianEDist_lt
- instIsRiemannianManifold
- Continuous.inner_bundle
- PseudoEMetricSpace.ofRiemannianMetric
- setOf_riemannianEDist_lt_subset_nhds'
- EMetricSpace.ofRiemannianMetric
- PseudoEmetricSpace.ofRiemannianMetric
- EmetricSpace.ofRiemannianMetric
- ContinuousOn.inner_bundle
Ancestors0
No ancestors.