From 7ac23e810defec6078dd75dd71fcbd30c307ac6a Mon Sep 17 00:00:00 2001 From: LehengChen Date: Sun, 14 Jun 2026 11:38:27 +0800 Subject: [PATCH 1/2] port(coordinate-ball): coordinate-ball chart predicates (IsCoordinateBall family) Ports the Lee Smooth Manifolds coordinate-ball predicates into the new OpenGALib/Manifold foundations domain. Pure addition, design-neutral (Mathlib ChartedSpace/IsManifold only), 0 sorry. Source: import/smooth-manifolds-lee @ a5f308c Chap01/Sec01/Definition_1_extra_2.lean Chap01/Sec01_03/Definition_1_3_extra_1.lean Co-Authored-By: Claude Opus 4.8 (1M context) --- OpenGALib.lean | 1 + OpenGALib/Manifold.lean | 10 + OpenGALib/Manifold/Charts/CoordinateBall.lean | 174 ++++++++++++++++++ 3 files changed, 185 insertions(+) create mode 100644 OpenGALib/Manifold.lean create mode 100644 OpenGALib/Manifold/Charts/CoordinateBall.lean diff --git a/OpenGALib.lean b/OpenGALib.lean index 7ccd3a3..83d39cb 100644 --- a/OpenGALib.lean +++ b/OpenGALib.lean @@ -1,4 +1,5 @@ import OpenGALib.Algebraic +import OpenGALib.Manifold import OpenGALib.Tensor import OpenGALib.MetricGeometry import OpenGALib.Riemannian diff --git a/OpenGALib/Manifold.lean b/OpenGALib/Manifold.lean new file mode 100644 index 0000000..f63f740 --- /dev/null +++ b/OpenGALib/Manifold.lean @@ -0,0 +1,10 @@ +import OpenGALib.Manifold.Charts.CoordinateBall + +/-! +# Manifold + +Manifold-foundations domain: chart-level and atlas-level structure on +topological and smooth manifolds, stated directly on Mathlib's +`ChartedSpace` / `IsManifold` API. Sits below `Riemannian` in the library +layering. Currently provides coordinate-ball predicates for charts. +-/ diff --git a/OpenGALib/Manifold/Charts/CoordinateBall.lean b/OpenGALib/Manifold/Charts/CoordinateBall.lean new file mode 100644 index 0000000..e5e670d --- /dev/null +++ b/OpenGALib/Manifold/Charts/CoordinateBall.lean @@ -0,0 +1,174 @@ +import Mathlib.Analysis.InnerProductSpace.PiL2 +import Mathlib.Geometry.Manifold.ChartedSpace +import Mathlib.Geometry.Manifold.ContMDiff.Atlas +import Mathlib.Geometry.Manifold.Instances.Real +import Mathlib.Topology.Bases +import Mathlib.Topology.Separation.Basic + +/-! +# Coordinate balls + +Coordinate-ball predicates for charts on a topological or smooth manifold. A +chart is a *coordinate ball* when its image is an open metric ball, a +*coordinate box* when its image is a product of open intervals, and *centered* +at a point when it sends that point to the origin. On a smooth manifold these +combine into the notions of a *smooth coordinate ball* (the source of a chart in +the maximal atlas whose image is an open ball) and a *regular coordinate ball* +(one whose closure sits inside a larger concentric chart). + +## Main definitions + +* `OpenPartialHomeomorph.IsCoordinateBall` — the chart's image is an open metric ball. +* `OpenPartialHomeomorph.IsCenteredAt` — the chart sends the point to `0`. +* `OpenPartialHomeomorph.IsCoordinateBox` — the chart's image is a product of open intervals. +* `OpenPartialHomeomorph.centerAt` — translate a chart so a source point maps to `0`. +* `Manifold.IsSmoothCoordinateBall` — source of a maximal-atlas chart whose image is an open ball. +* `Manifold.IsRegularCoordinateBall` — a coordinate ball whose closure sits in a larger chart. + +## Main results + +* `OpenPartialHomeomorph.isCoordinateBall_of_target_eq_ball` — a chart with ball image is a coordinate ball. +* `OpenPartialHomeomorph.isCoordinateBox_of_target_eq` — a chart with box image is a coordinate box. +* `OpenPartialHomeomorph.centerAt_isCenteredAt` — the centered chart is centered at its point. +* `Manifold.IsRegularCoordinateBall.exists_smoothCoordinateBall_superset` — a regular + coordinate ball lies in a surrounding smooth coordinate ball. + +Reference: Lee, *Introduction to Smooth Manifolds*, §1. + +Ported from SmoothManifoldsLee Chap01/Sec01/Definition_1_extra_2.lean (a5f308c) +Ported from SmoothManifoldsLee Chap01/Sec01_03/Definition_1_3_extra_1.lean (a5f308c) +-/ + +noncomputable section + +open Set +open scoped Manifold Topology + +universe u v + +section Charts + +variable {H : Type*} [PseudoMetricSpace H] +variable {n : ℕ} {M : Type u} [TopologicalSpace M] + +/-- **Math.** The chart `e` is a *coordinate ball*: its image is some open metric +ball `Metric.ball c r` of positive radius. **Eng.** Predicate on +`OpenPartialHomeomorph M H`; existentially quantifies over a center `c` and radius +`r` with `e.target = Metric.ball c r`. Stated on Mathlib's metric-space chart so it +applies to any model space, not just `EuclideanSpace`. -/ +def OpenPartialHomeomorph.IsCoordinateBall (e : OpenPartialHomeomorph M H) : Prop := + ∃ c : H, ∃ r : ℝ, 0 < r ∧ e.target = Metric.ball c r + +/-- **Math.** A chart whose image is the open ball `Metric.ball c r` is a coordinate +ball. **Eng.** Introduction rule for `IsCoordinateBall`: feed the witnessing center, +radius, positivity and target equality straight into the existential. -/ +theorem OpenPartialHomeomorph.isCoordinateBall_of_target_eq_ball + (e : OpenPartialHomeomorph M H) (c : H) (r : ℝ) (hr : 0 < r) + (h : e.target = Metric.ball c r) : e.IsCoordinateBall := + ⟨c, r, hr, h⟩ + +variable (e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) + +/-- **Math.** The chart `e` is *centered at* `p`: the point `p` lies in the chart's +source and `e` sends it to the origin `0`. **Eng.** Predicate packaging +`p ∈ e.source` with the coordinate condition `e p = 0`; the codomain is the +Euclidean model space so `0` is the literal zero vector. -/ +def OpenPartialHomeomorph.IsCenteredAt (p : M) : Prop := + p ∈ e.source ∧ e p = 0 + +/-- **Math.** The chart `e` is a *coordinate box*: its image is a product of open +intervals `∏ᵢ (aᵢ, bᵢ)`. **Eng.** Existential over endpoint vectors `a b` with +`a i < b i` coordinatewise and `e.target` equal to the set of points whose every +coordinate lies in the corresponding `Set.Ioo`. -/ +def OpenPartialHomeomorph.IsCoordinateBox : Prop := + ∃ a b : EuclideanSpace ℝ (Fin n), + (∀ i, a i < b i) ∧ e.target = { x | ∀ i : Fin n, x i ∈ Set.Ioo (a i) (b i) } + +/-- **Math.** A chart whose image is the open box `∏ᵢ (aᵢ, bᵢ)` is a coordinate box. +**Eng.** Introduction rule for `IsCoordinateBox`: supply the endpoint vectors, the +coordinatewise strict-order hypothesis and the target equality to the existential. -/ +theorem OpenPartialHomeomorph.isCoordinateBox_of_target_eq + (e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) + (a b : EuclideanSpace ℝ (Fin n)) + (hab : ∀ i, a i < b i) + (h : e.target = { x | ∀ i : Fin n, x i ∈ Set.Ioo (a i) (b i) }) : e.IsCoordinateBox := + ⟨a, b, hab, h⟩ + +/-- **Math.** *Center* the chart `e` at a source point `p`, producing a chart with +the same source that sends `p` to the origin. **Eng.** Postcompose `e` with the +translation homeomorphism `Homeomorph.addRight (-e p)` via `transHomeomorph`; this +shifts coordinates so the image of `p` becomes `0` while leaving the source set +unchanged. -/ +def OpenPartialHomeomorph.centerAt (p : e.source) : + OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)) := + e.transHomeomorph (Homeomorph.addRight (-e p)) + +/-- **Math.** Centering a chart leaves its domain of definition unchanged. **Eng.** +The translation only affects the codomain, so `(e.centerAt p).source = e.source` +holds definitionally; `@[simp]` so downstream goals reduce automatically. -/ +@[simp] theorem OpenPartialHomeomorph.centerAt_source (p : e.source) : + (e.centerAt p).source = e.source := + rfl + +/-- **Math.** The chart obtained by centering `e` at `p` is indeed centered at `p`. +**Eng.** Membership of `p` in the source is unchanged; the coordinate condition +`(e.centerAt p) p = 0` follows from unfolding `centerAt` and simplifying the +translation by `-e p`. -/ +theorem OpenPartialHomeomorph.centerAt_isCenteredAt (p : e.source) : + (e.centerAt p).IsCenteredAt p := by + exact ⟨p.2, by simp [OpenPartialHomeomorph.centerAt]⟩ + +end Charts + +namespace Manifold + +variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] +variable {M : Type v} [TopologicalSpace M] [ChartedSpace E M] +variable [IsManifold (modelWithCornersSelf ℝ E) (⊤ : WithTop ℕ∞) M] + +/-- **Math.** A *smooth coordinate ball* is a subset `B ⊆ M` that is the source of a +chart in the maximal smooth atlas whose image is an open metric ball in the model +space `E`. **Eng.** Existential over a chart `φ` lying in +`IsManifold.maximalAtlas` with `φ.source = B` and `φ.IsCoordinateBall`. Stated on +Mathlib's `ChartedSpace`/`IsManifold` over `modelWithCornersSelf ℝ E`, with no +OpenGA packaging class. -/ +def IsSmoothCoordinateBall (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] + {M : Type v} [TopologicalSpace M] [ChartedSpace E M] + [IsManifold (modelWithCornersSelf ℝ E) (⊤ : WithTop ℕ∞) M] (B : Set M) : Prop := + ∃ φ : OpenPartialHomeomorph M E, + φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℝ E) (⊤ : WithTop ℕ∞) M ∧ + φ.source = B ∧ φ.IsCoordinateBall + +/-- **Math.** A *regular coordinate ball* is a subset `B` whose closure lies inside a +larger maximal-atlas chart that sends `B` and its closure to concentric open and +closed balls of radius `r`, while the chart's whole image is a strictly larger ball +of radius `r' > r`. **Eng.** Existential over a chart and radii `r < r'` recording +`chart '' B = Metric.ball 0 r`, `chart '' closure B = Metric.closedBall 0 r`, and +`chart.target = Metric.ball 0 r'`, all in the model space `E`. -/ +def IsRegularCoordinateBall (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] + {M : Type v} [TopologicalSpace M] [ChartedSpace E M] + [IsManifold (modelWithCornersSelf ℝ E) (⊤ : WithTop ℕ∞) M] (B : Set M) : Prop := + ∃ chart : OpenPartialHomeomorph M E, + chart ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℝ E) (⊤ : WithTop ℕ∞) M ∧ + closure B ⊆ chart.source ∧ + ∃ r r' : ℝ, + 0 < r ∧ + r < r' ∧ + chart '' B = Metric.ball (0 : E) r ∧ + chart '' closure B = Metric.closedBall (0 : E) r ∧ + chart.target = Metric.ball (0 : E) r' + +/-- **Math.** Every regular coordinate ball is contained in a surrounding smooth +coordinate ball: namely the source of its defining larger chart, which itself is a +smooth coordinate ball, and which contains the closure of `B`. **Eng.** Destructure +the regular-ball witness, take `B' := chart.source`, and rebuild the smooth-ball +data from the same chart using `isCoordinateBall_of_target_eq_ball` with radius `r'` +(positive since `0 < r < r'`). -/ +theorem IsRegularCoordinateBall.exists_smoothCoordinateBall_superset {B : Set M} + (hB : IsRegularCoordinateBall E B) : + ∃ B' : Set M, IsSmoothCoordinateBall E B' ∧ closure B ⊆ B' := by + rcases hB with ⟨chart, hchart, hclosure, r, r', hr, hr', -, -, htarget⟩ + refine ⟨chart.source, ⟨chart, hchart, rfl, ?_⟩, hclosure⟩ + exact chart.isCoordinateBall_of_target_eq_ball (0 : E) r' (lt_trans hr hr') htarget + +end Manifold From db767b148567c501016ea6c55639bcc3653d27d7 Mon Sep 17 00:00:00 2001 From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com> Date: Sun, 14 Jun 2026 14:44:33 -0400 Subject: [PATCH 2/2] docs(coordinate-ball): house-style docstrings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Anchor-file convention: single **Math.** tags only (no **Eng.** prose), module docstring organised by architectural layer (model-generic → Euclidean → smooth-manifold) rather than textbook order, provenance demoted to a one-line footer. Statements and proofs unchanged. --- OpenGALib/Manifold/Charts/CoordinateBall.lean | 92 ++++++++----------- 1 file changed, 36 insertions(+), 56 deletions(-) diff --git a/OpenGALib/Manifold/Charts/CoordinateBall.lean b/OpenGALib/Manifold/Charts/CoordinateBall.lean index e5e670d..56de54a 100644 --- a/OpenGALib/Manifold/Charts/CoordinateBall.lean +++ b/OpenGALib/Manifold/Charts/CoordinateBall.lean @@ -8,13 +8,20 @@ import Mathlib.Topology.Separation.Basic /-! # Coordinate balls -Coordinate-ball predicates for charts on a topological or smooth manifold. A -chart is a *coordinate ball* when its image is an open metric ball, a -*coordinate box* when its image is a product of open intervals, and *centered* -at a point when it sends that point to the origin. On a smooth manifold these -combine into the notions of a *smooth coordinate ball* (the source of a chart in -the maximal atlas whose image is an open ball) and a *regular coordinate ball* -(one whose closure sits inside a larger concentric chart). +Chart-shape predicates and constructions, layered by how much ambient +structure they need so downstream code imports only the generality it uses: + +1. **Model-generic** — `IsCoordinateBall` is stated over any metric model + space, not just `EuclideanSpace`; it is the reusable base every other + layer builds on. +2. **Euclidean charts** — `IsCenteredAt`, `IsCoordinateBox`, `centerAt` + need coordinates and an origin, so they specialise to the Euclidean model. +3. **Smooth-manifold layer** — `IsSmoothCoordinateBall` and + `IsRegularCoordinateBall` build on the maximal smooth atlas; these are the + interface consumed by covering and partition-of-unity arguments. The + "collar room" of a regular coordinate ball is the reusable payload; the + predicate itself is mostly a stepping stone to + `IsRegularCoordinateBall.exists_smoothCoordinateBall_superset`. ## Main definitions @@ -33,10 +40,7 @@ the maximal atlas whose image is an open ball) and a *regular coordinate ball* * `Manifold.IsRegularCoordinateBall.exists_smoothCoordinateBall_superset` — a regular coordinate ball lies in a surrounding smooth coordinate ball. -Reference: Lee, *Introduction to Smooth Manifolds*, §1. - -Ported from SmoothManifoldsLee Chap01/Sec01/Definition_1_extra_2.lean (a5f308c) -Ported from SmoothManifoldsLee Chap01/Sec01_03/Definition_1_3_extra_1.lean (a5f308c) +Provenance: SmoothManifoldsLee a5f308c — Definition_1_extra_2, Definition_1_3_extra_1. -/ noncomputable section @@ -51,17 +55,14 @@ section Charts variable {H : Type*} [PseudoMetricSpace H] variable {n : ℕ} {M : Type u} [TopologicalSpace M] -/-- **Math.** The chart `e` is a *coordinate ball*: its image is some open metric -ball `Metric.ball c r` of positive radius. **Eng.** Predicate on -`OpenPartialHomeomorph M H`; existentially quantifies over a center `c` and radius -`r` with `e.target = Metric.ball c r`. Stated on Mathlib's metric-space chart so it -applies to any model space, not just `EuclideanSpace`. -/ +/-- **Math.** The chart `e` is a *coordinate ball*: its image is an open metric ball +`Metric.ball c r` of positive radius. Stated over any metric model space, so it +applies beyond `EuclideanSpace`. -/ def OpenPartialHomeomorph.IsCoordinateBall (e : OpenPartialHomeomorph M H) : Prop := ∃ c : H, ∃ r : ℝ, 0 < r ∧ e.target = Metric.ball c r -/-- **Math.** A chart whose image is the open ball `Metric.ball c r` is a coordinate -ball. **Eng.** Introduction rule for `IsCoordinateBall`: feed the witnessing center, -radius, positivity and target equality straight into the existential. -/ +/-- **Math.** A chart whose image is a given open ball `Metric.ball c r` is a +coordinate ball. -/ theorem OpenPartialHomeomorph.isCoordinateBall_of_target_eq_ball (e : OpenPartialHomeomorph M H) (c : H) (r : ℝ) (hr : 0 < r) (h : e.target = Metric.ball c r) : e.IsCoordinateBall := @@ -69,24 +70,19 @@ theorem OpenPartialHomeomorph.isCoordinateBall_of_target_eq_ball variable (e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) -/-- **Math.** The chart `e` is *centered at* `p`: the point `p` lies in the chart's -source and `e` sends it to the origin `0`. **Eng.** Predicate packaging -`p ∈ e.source` with the coordinate condition `e p = 0`; the codomain is the -Euclidean model space so `0` is the literal zero vector. -/ +/-- **Math.** The chart `e` is *centered at* `p`: the point `p` lies in its source +and `e` sends it to the origin `0`. -/ def OpenPartialHomeomorph.IsCenteredAt (p : M) : Prop := p ∈ e.source ∧ e p = 0 /-- **Math.** The chart `e` is a *coordinate box*: its image is a product of open -intervals `∏ᵢ (aᵢ, bᵢ)`. **Eng.** Existential over endpoint vectors `a b` with -`a i < b i` coordinatewise and `e.target` equal to the set of points whose every -coordinate lies in the corresponding `Set.Ioo`. -/ +intervals `∏ᵢ (aᵢ, bᵢ)`. -/ def OpenPartialHomeomorph.IsCoordinateBox : Prop := ∃ a b : EuclideanSpace ℝ (Fin n), (∀ i, a i < b i) ∧ e.target = { x | ∀ i : Fin n, x i ∈ Set.Ioo (a i) (b i) } -/-- **Math.** A chart whose image is the open box `∏ᵢ (aᵢ, bᵢ)` is a coordinate box. -**Eng.** Introduction rule for `IsCoordinateBox`: supply the endpoint vectors, the -coordinatewise strict-order hypothesis and the target equality to the existential. -/ +/-- **Math.** A chart whose image is a given open box `∏ᵢ (aᵢ, bᵢ)` is a coordinate +box. -/ theorem OpenPartialHomeomorph.isCoordinateBox_of_target_eq (e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) (a b : EuclideanSpace ℝ (Fin n)) @@ -94,26 +90,18 @@ theorem OpenPartialHomeomorph.isCoordinateBox_of_target_eq (h : e.target = { x | ∀ i : Fin n, x i ∈ Set.Ioo (a i) (b i) }) : e.IsCoordinateBox := ⟨a, b, hab, h⟩ -/-- **Math.** *Center* the chart `e` at a source point `p`, producing a chart with -the same source that sends `p` to the origin. **Eng.** Postcompose `e` with the -translation homeomorphism `Homeomorph.addRight (-e p)` via `transHomeomorph`; this -shifts coordinates so the image of `p` becomes `0` while leaving the source set -unchanged. -/ +/-- **Math.** *Center* the chart `e` at a source point `p`: the chart with the same +source that sends `p` to the origin. -/ def OpenPartialHomeomorph.centerAt (p : e.source) : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)) := e.transHomeomorph (Homeomorph.addRight (-e p)) -/-- **Math.** Centering a chart leaves its domain of definition unchanged. **Eng.** -The translation only affects the codomain, so `(e.centerAt p).source = e.source` -holds definitionally; `@[simp]` so downstream goals reduce automatically. -/ +/-- **Math.** Centering a chart leaves its domain of definition unchanged. -/ @[simp] theorem OpenPartialHomeomorph.centerAt_source (p : e.source) : (e.centerAt p).source = e.source := rfl -/-- **Math.** The chart obtained by centering `e` at `p` is indeed centered at `p`. -**Eng.** Membership of `p` in the source is unchanged; the coordinate condition -`(e.centerAt p) p = 0` follows from unfolding `centerAt` and simplifying the -translation by `-e p`. -/ +/-- **Math.** The chart obtained by centering `e` at `p` is centered at `p`. -/ theorem OpenPartialHomeomorph.centerAt_isCenteredAt (p : e.source) : (e.centerAt p).IsCenteredAt p := by exact ⟨p.2, by simp [OpenPartialHomeomorph.centerAt]⟩ @@ -128,10 +116,7 @@ variable [IsManifold (modelWithCornersSelf ℝ E) (⊤ : WithTop ℕ∞) M] /-- **Math.** A *smooth coordinate ball* is a subset `B ⊆ M` that is the source of a chart in the maximal smooth atlas whose image is an open metric ball in the model -space `E`. **Eng.** Existential over a chart `φ` lying in -`IsManifold.maximalAtlas` with `φ.source = B` and `φ.IsCoordinateBall`. Stated on -Mathlib's `ChartedSpace`/`IsManifold` over `modelWithCornersSelf ℝ E`, with no -OpenGA packaging class. -/ +space `E`. -/ def IsSmoothCoordinateBall (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type v} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (⊤ : WithTop ℕ∞) M] (B : Set M) : Prop := @@ -139,12 +124,10 @@ def IsSmoothCoordinateBall (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℝ E) (⊤ : WithTop ℕ∞) M ∧ φ.source = B ∧ φ.IsCoordinateBall -/-- **Math.** A *regular coordinate ball* is a subset `B` whose closure lies inside a -larger maximal-atlas chart that sends `B` and its closure to concentric open and -closed balls of radius `r`, while the chart's whole image is a strictly larger ball -of radius `r' > r`. **Eng.** Existential over a chart and radii `r < r'` recording -`chart '' B = Metric.ball 0 r`, `chart '' closure B = Metric.closedBall 0 r`, and -`chart.target = Metric.ball 0 r'`, all in the model space `E`. -/ +/-- **Math.** A *regular coordinate ball* is a subset `B` with collar room: a +maximal-atlas chart sends `B` to an open ball of radius `r`, its closure to the +concentric closed ball of radius `r`, and the whole chart image to a strictly +larger ball of radius `r' > r`. -/ def IsRegularCoordinateBall (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] {M : Type v} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf ℝ E) (⊤ : WithTop ℕ∞) M] (B : Set M) : Prop := @@ -159,11 +142,8 @@ def IsRegularCoordinateBall (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ chart.target = Metric.ball (0 : E) r' /-- **Math.** Every regular coordinate ball is contained in a surrounding smooth -coordinate ball: namely the source of its defining larger chart, which itself is a -smooth coordinate ball, and which contains the closure of `B`. **Eng.** Destructure -the regular-ball witness, take `B' := chart.source`, and rebuild the smooth-ball -data from the same chart using `isCoordinateBall_of_target_eq_ball` with radius `r'` -(positive since `0 < r < r'`). -/ +coordinate ball — the source of its defining larger chart, which contains the +closure of `B`. -/ theorem IsRegularCoordinateBall.exists_smoothCoordinateBall_superset {B : Set M} (hB : IsRegularCoordinateBall E B) : ∃ B' : Set M, IsSmoothCoordinateBall E B' ∧ closure B ⊆ B' := by