Full support of Riemannian volume

The Riemannian volume measure of a continuous finite-dimensional Riemannian manifold is positive on nonempty open sets. This gives the full-support interface used by later integration and positivity arguments.

instance TauCeti.isOpenPosMeasure_riemannianVolume {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [MeasurableSpace M] [BorelSpace M] [LindelofSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] : (riemannianVolume I M).IsOpenPosMeasure

Riemannian volume is positive on every nonempty open set.