Riemannian metric balls are open in the manifold topology

Proved

Riemannian.RiemannianMetric.isOpen_geodesicBall

by Xinze-Li-Moqian · Sep 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

comparison-geometrypoincare-foundationsriemannian-geometry

Let $M$ be a smooth Hausdorff, $\sigma$ -compact manifold with a finite-dimensional real inner-product model space, and let $g$ be a smooth Riemannian metric. For every $p\in M$ and $r\in\mathbb R$ , the metric ball $B_g(p,r)$ is open in the original manifold topology. Completeness, connectedness and curvature assumptions are not required. This identifies the ball interface with the topology needed for local volume estimates.

Preamble

import Definitions.Def_OpenGA_GeodesicBall
import Mathlib.Geometry.Manifold.Metrizable

noncomputable section
set_option autoImplicit false

open Bundle Set DifferentialGeometry
open scoped Manifold ContDiff ENNReal

open Riemannian Riemannian.RiemannianMetric

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  {H : Type*} [TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  {M : Type*} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]

Formal statement

theorem Riemannian.RiemannianMetric.isOpen_geodesicBall [FiniteDimensional ℝ E] [T2Space M] [SigmaCompactSpace M]
    (g : RiemannianMetric I M) (p : M) (r : ℝ) :
    IsOpen (g.geodesicBall p r) := by sorry

Source

https://github.com/MathNetwork/OpenGA/blob/16e60c2b09f5c1d3c2bf44ed81429b1a1fecc1b8/OpenGALib/ComparisonGeometry/MetricBall.lean#L63-L78

View graph