Structures · Geometry

IsRiemannianManifold

Consider a manifold in which the tangent spaces are already endowed with an inner product, and the space is already endowed with an extended distance. We say that this is a Riemannian manifold if the distance is given by the infimum of the lengths of C^1 paths, measured using the norm in the tangent spaces. This is a Prop-valued typeclass, on top of existing data. If you need to construct a distance using a Riemannian structure, see EMetricSpace.ofRiemannianMetric.

Defined in

Mathlib.Geometry.Manifold.Riemannian.Basic

Shape

2 explicit arguments · adds out