From fb3503dfcf668b0ae63d7476bf9c22a75c639b34 Mon Sep 17 00:00:00 2001 From: LehengChen Date: Sun, 14 Jun 2026 12:27:14 +0800 Subject: [PATCH 1/4] port(precompact-basis): precompact coordinate balls + locally finite refinement MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Port Lee Lemma 1.10 (countable precompact-coordinate-ball basis) and Theorem 1.15 (countable locally finite refinement subordinate to any open cover) into OpenGALib/Manifold/Charts/PrecompactBasis.lean. The source binder [TopologicalManifold n M] is restated as the four Mathlib classes [TopologicalSpace M] [T2Space M] [SecondCountableTopology M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M]; the TopologicalManifold.locallyCompactSpace_of_topologicalManifold projection is re-pointed to ChartedSpace.locallyCompactSpace. Co-Authored-By: Claude Opus 4.8 (1M context) --- OpenGALib/Manifold.lean | 1 + .../Manifold/Charts/PrecompactBasis.lean | 295 ++++++++++++++++++ 2 files changed, 296 insertions(+) create mode 100644 OpenGALib/Manifold/Charts/PrecompactBasis.lean diff --git a/OpenGALib/Manifold.lean b/OpenGALib/Manifold.lean index f63f740..3b671a6 100644 --- a/OpenGALib/Manifold.lean +++ b/OpenGALib/Manifold.lean @@ -1,4 +1,5 @@ import OpenGALib.Manifold.Charts.CoordinateBall +import OpenGALib.Manifold.Charts.PrecompactBasis /-! # Manifold diff --git a/OpenGALib/Manifold/Charts/PrecompactBasis.lean b/OpenGALib/Manifold/Charts/PrecompactBasis.lean new file mode 100644 index 0000000..4ed5f77 --- /dev/null +++ b/OpenGALib/Manifold/Charts/PrecompactBasis.lean @@ -0,0 +1,295 @@ +import Mathlib.Analysis.InnerProductSpace.PiL2 +import Mathlib.Geometry.Manifold.ChartedSpace +import Mathlib.Geometry.Manifold.Instances.Real +import Mathlib.Topology.Bases +import Mathlib.Topology.Compactness.Paracompact +import Mathlib.Topology.Compactness.SigmaCompact +import Mathlib.Topology.Separation.Basic +import Mathlib.Topology.Sets.OpenCover +import OpenGALib.Manifold.Charts.CoordinateBall + +/-! +# Precompact coordinate balls and locally finite refinements + +A *precompact coordinate ball* is the source of a coordinate-ball chart whose +closure is compact. On a topological `n`-manifold — a Hausdorff, second-countable +space charted over `EuclideanSpace ℝ (Fin n)` — these sets form a basis for the +topology, and second countability thins this basis to a countable one (Lee's +Lemma 1.10). Combined with paracompactness, every open cover of such a manifold +admits a countable, locally finite refinement by precompact coordinate balls +subordinate to the cover (Lee's Theorem 1.15). + +## Main definitions + +* `Manifold.IsPrecompactCoordinateBall` — source of a coordinate-ball chart with compact closure. + +## Main results + +* `Manifold.IsPrecompactCoordinateBall.isOpen` — a precompact coordinate ball is open. +* `Manifold.isTopologicalBasis_isPrecompactCoordinateBall` — precompact coordinate balls form a basis. +* `Manifold.exists_countable_precompact_coordinate_ball_basis` — that basis can be taken countable. +* `Manifold.paracompactSpace_of_manifold` — a topological manifold is paracompact. +* `Manifold.exists_countable_locally_finite_precompact_coordinate_ball_refinement` — + every open cover has a countable locally finite refinement by precompact coordinate balls. + +Reference: Lee, *Introduction to Smooth Manifolds*, §1 (Lemma 1.10, Theorem 1.15). + +Ported from SmoothManifoldsLee Chap01/Sec01/Lemma_1_10.lean (a5f308c) +Ported from SmoothManifoldsLee Chap01/Sec01/Theorem_1_15.lean (a5f308c) +-/ + +open Set TopologicalSpace +open scoped Topology + +universe u v + +namespace Manifold + +section Basis + +variable {n : ℕ} {M : Type u} [TopologicalSpace M] + +/-- **Math.** A set `s ⊆ M` is a *precompact coordinate ball*: it is the source of +some coordinate-ball chart and its closure is compact. **Eng.** Conjunction of an +existential over a chart `e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))` +with `e.source = s` and `e.IsCoordinateBall`, together with +`IsCompact (closure s)`. Stated purely on Mathlib's chart/compactness API. -/ +def IsPrecompactCoordinateBall (n : ℕ) (s : Set M) : Prop := + (∃ e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)), + e.source = s ∧ e.IsCoordinateBall) ∧ + IsCompact (closure s) + +/-- **Math.** A precompact coordinate ball is open. **Eng.** Extract the witnessing +chart `e` with `e.source = s`; the source of an open partial homeomorphism is open +(`e.open_source`), so rewriting along `e.source = s` closes the goal. -/ +theorem IsPrecompactCoordinateBall.isOpen {s : Set M} + (hs : IsPrecompactCoordinateBall n s) : IsOpen s := by + rcases hs.1 with ⟨e, rfl, -⟩ + simpa using e.open_source + +/-- **Math.** A precompact coordinate ball has compact closure. **Eng.** Projection +onto the compact-closure component of the defining conjunction. -/ +theorem IsPrecompactCoordinateBall.isCompact_closure {s : Set M} + (hs : IsPrecompactCoordinateBall n s) : IsCompact (closure s) := + hs.2 + +variable [T2Space M] [SecondCountableTopology M] + [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] + +omit [SecondCountableTopology M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] in +/-- **Math.** Restricting a chart to a Euclidean open ball whose closed ball is +compactly contained in the chart target produces a precompact coordinate ball in +`M`. **Eng.** Restrict `e` to `Metric.ball c r` via `trans (OpenPartialHomeomorph.ofSet …)`; +identify the restricted source/target, get compactness of the closure from the +compact closed ball pushed through the continuous inverse chart, and exhibit the +coordinate-ball witness with `isCoordinateBall_of_target_eq_ball`. The +`[TopologicalManifold n M]` binder of the source is restated as the four Mathlib +classes `[T2Space M] [SecondCountableTopology M] [ChartedSpace … M]`; here only +`[T2Space M]` (for compactness of the closure) is needed beyond the ambient +topology, so the second-countable and charted-space instances are `omit`ted. -/ +theorem isPrecompactCoordinateBall_chart_preimage_metric_ball + (e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) {c : EuclideanSpace ℝ (Fin n)} + {r : ℝ} (hr : 0 < r) (hclosed : Metric.closedBall c r ⊆ e.target) : + IsPrecompactCoordinateBall n (e.symm '' Metric.ball c r) := by + let e' := e.trans (OpenPartialHomeomorph.ofSet (Metric.ball c r) Metric.isOpen_ball) + have hball_target : Metric.ball c r ⊆ e.target := by + exact (Metric.ball_subset_closedBall : Metric.ball c r ⊆ Metric.closedBall c r).trans hclosed + have hsource : e'.source = e.symm '' Metric.ball c r := by + -- The restricted chart is defined exactly on the inverse image of the chosen ball. + dsimp [e'] + exact (e.symm_image_eq_source_inter_preimage hball_target).symm + have htarget : e'.target = Metric.ball c r := by + -- On the target side, the restriction keeps precisely the chosen Euclidean ball. + dsimp [e'] + exact inter_eq_left.2 hball_target + have hcompactCarrier : IsCompact (e.symm '' Metric.closedBall c r) := by + -- The closed ball is compact in Euclidean space, and the inverse chart is continuous on it. + exact (isCompact_closedBall (x := c) (r := r)).image_of_continuousOn + (e.continuousOn_symm.mono hclosed) + have hclosureCompact : IsCompact (closure (e.symm '' Metric.ball c r)) := by + -- The closure stays inside the compact pullback of the closed Euclidean ball. + exact hcompactCarrier.closure_of_subset + (Set.image_mono (Metric.ball_subset_closedBall : Metric.ball c r ⊆ Metric.closedBall c r)) + refine ⟨?_, hclosureCompact⟩ + refine ⟨e', hsource, ?_⟩ + exact OpenPartialHomeomorph.isCoordinateBall_of_target_eq_ball e' c r hr htarget + +omit [SecondCountableTopology M] in +/-- **Math.** Every point of an open set lies in a precompact coordinate ball +contained in that open set. **Eng.** Work in the preferred chart `e := chartAt … x`: +its image of `e.source ∩ u` is open, so a small closed Euclidean ball around `e x` +sits inside it; pulling the corresponding open ball back through `e` gives the +required precompact coordinate ball, using +`isPrecompactCoordinateBall_chart_preimage_metric_ball`. -/ +theorem exists_isPrecompactCoordinateBall_subset_of_mem_open {x : M} + {u : Set M} (hx : x ∈ u) (hu : IsOpen u) : + ∃ s : Set M, IsPrecompactCoordinateBall n s ∧ x ∈ s ∧ s ⊆ u := by + let e := chartAt (EuclideanSpace ℝ (Fin n)) x + let y : EuclideanSpace ℝ (Fin n) := e x + let w : Set (EuclideanSpace ℝ (Fin n)) := e '' (e.source ∩ u) + have hxsource : x ∈ e.source := mem_chart_source _ x + have hyw : y ∈ w := by + refine ⟨x, ⟨hxsource, hx⟩, rfl⟩ + have hw_open : IsOpen w := by + -- The image of the open neighborhood inside the chart source is open in Euclidean space. + simpa [w] using e.isOpen_image_source_inter hu + obtain ⟨r, hr, hclosed⟩ : + ∃ r : ℝ, 0 < r ∧ Metric.closedBall y r ⊆ w := by + -- Choose a small closed Euclidean ball around the charted point inside that open image. + exact Metric.nhds_basis_closedBall.mem_iff.1 (hw_open.mem_nhds hyw) + have hw_target : w ⊆ e.target := by + -- The chart image of any subset of the source stays in the chart target. + simpa [w] using (Set.image_mono (show e.source ∩ u ⊆ e.source from inter_subset_left)).trans + e.image_source_eq_target.subset + let s : Set M := e.symm '' Metric.ball y r + have hs_precompact : IsPrecompactCoordinateBall n s := by + -- Pull back the chosen Euclidean ball through the chart. + simpa [s, y] using isPrecompactCoordinateBall_chart_preimage_metric_ball + (n := n) e hr (hclosed.trans hw_target) + have hxs : x ∈ s := by + -- The charted point lies in every positive-radius ball centered at itself. + refine ⟨y, Metric.mem_ball_self hr, ?_⟩ + simpa [y] using e.left_inv hxsource + have hs_subset_source_u : s ⊆ e.source ∩ u := by + -- The pulled-back ball lies inside the original open neighborhood because its image does. + have hball_w : Metric.ball y r ⊆ w := by + exact (Metric.ball_subset_closedBall : Metric.ball y r ⊆ Metric.closedBall y r).trans hclosed + change e.symm '' Metric.ball y r ⊆ e.source ∩ u + refine (Set.image_mono hball_w).trans ?_ + have himage : e.symm '' w = e.source ∩ u := by + simpa [w] using e.symm_image_image_of_subset_source + (s := e.source ∩ u) (show e.source ∩ u ⊆ e.source from inter_subset_left) + exact himage.subset + exact ⟨s, hs_precompact, hxs, fun z hz ↦ (hs_subset_source_u hz).2⟩ + +omit [SecondCountableTopology M] in +/-- **Math.** Precompact coordinate balls form a topological basis on a topological +manifold. **Eng.** Use `isTopologicalBasis_of_isOpen_of_nhds`: each precompact +coordinate ball is open, and `exists_isPrecompactCoordinateBall_subset_of_mem_open` +supplies a basis element inside every open neighborhood of every point. -/ +theorem isTopologicalBasis_isPrecompactCoordinateBall : + IsTopologicalBasis { s : Set M | IsPrecompactCoordinateBall n s } := by + -- The local chart construction gives a basis element inside every open neighborhood. + refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_ + · intro s hs + exact hs.isOpen + · intro x u hx hu + obtain ⟨s, hs, hxs, hsu⟩ := exists_isPrecompactCoordinateBall_subset_of_mem_open + (n := n) hx hu + exact ⟨s, hs, hxs, hsu⟩ + +/-- **Math.** Lemma 1.10: every topological manifold has a *countable* topological +basis consisting of precompact coordinate balls. **Eng.** Start from the (possibly +uncountable) basis `isTopologicalBasis_isPrecompactCoordinateBall`; second +countability lets `IsTopologicalBasis.exists_countable` thin it to a countable +subfamily, every member of which is still a precompact coordinate ball. -/ +theorem exists_countable_precompact_coordinate_ball_basis : + ∃ b : Set (Set M), + b.Countable ∧ IsTopologicalBasis b ∧ ∀ s ∈ b, IsPrecompactCoordinateBall n s := by + let B : Set (Set M) := { s : Set M | IsPrecompactCoordinateBall n s } + have hB : IsTopologicalBasis B := isTopologicalBasis_isPrecompactCoordinateBall (n := n) + -- Once the local basis is available, second countability lets us thin it to a countable subbasis. + obtain ⟨b, hbB, hbCountable, hbBasis⟩ := hB.exists_countable + exact ⟨b, hbCountable, hbBasis, fun s hs ↦ hbB hs⟩ + +end Basis + +section Refinement + +variable {n : ℕ} {M : Type u} [TopologicalSpace M] [T2Space M] + [SecondCountableTopology M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] + +include n in +/-- **Math.** A topological manifold is paracompact. **Eng.** It is locally compact +because charted over the locally compact `EuclideanSpace ℝ (Fin n)` +(`ChartedSpace.locallyCompactSpace`), and second-countable by hypothesis, hence +sigma-compact (`sigmaCompactSpace_of_locallyCompact_secondCountable`); a locally +compact, sigma-compact Hausdorff space is paracompact. The source's +`TopologicalManifold.locallyCompactSpace_of_topologicalManifold` projection is +re-pointed to the Mathlib lemma `ChartedSpace.locallyCompactSpace`. -/ +theorem paracompactSpace_of_manifold : ParacompactSpace M := by + letI : LocallyCompactSpace M := + ChartedSpace.locallyCompactSpace (EuclideanSpace ℝ (Fin n)) M + letI : SigmaCompactSpace M := sigmaCompactSpace_of_locallyCompact_secondCountable + infer_instance + +/-- **Math.** Companion bridge: given an open cover of a locally compact, +sigma-compact, Hausdorff space and any basis for its topology, there is a countable +locally finite refinement by basis elements subordinate to the cover. **Eng.** +Pick, at each point, a cover member containing it; build subordinate neighborhood +bases from `hB` and feed them to Mathlib's +`refinement_of_locallyCompact_sigmaCompact_of_nhds_basis`; local finiteness yields +countability of the index. Placed in `namespace Manifold` (the source put it in the +Mathlib type namespace `TopologicalSpace.IsOpenCover` for `hU.…` dot notation; we +keep the declaration name but state it as a plain theorem to stay inside the +project namespace whitelist — see PR description). -/ +theorem exists_countable_locallyFinite_refinement_of_isTopologicalBasis {X : Type u} + [TopologicalSpace X] [LocallyCompactSpace X] [SigmaCompactSpace X] [T2Space X] + {ι : Type v} {U : ι → Opens X} + (hU : IsOpenCover U) {B : Set (Set X)} (hB : IsTopologicalBasis B) : + ∃ (κ : Type u), Countable κ ∧ ∃ V : κ → Opens X, + IsOpenCover V ∧ LocallyFinite (fun j ↦ (V j : Set X)) ∧ + (∀ j, (V j : Set X) ∈ B) ∧ + (∀ j, ∃ i, (V j : Set X) ⊆ U i) := by + -- Choose, at each point, one member of the original cover that contains that point. + choose i hi using fun x : X ↦ hU.exists_mem_nhds x + have hBU : + ∀ x : X, + (𝓝 x).HasBasis + (fun s : Set X ↦ s ∈ B ∧ x ∈ s ∧ s ⊆ U (i x)) + id := by + intro x + let hxB : (𝓝 x).HasBasis (fun s : Set X ↦ s ∈ B ∧ x ∈ s) id := hB.nhds_hasBasis + simpa [and_assoc] using hxB.restrict_subset (hi x) + -- Feed the subordinate neighborhood bases into the standard locally finite refinement theorem. + rcases refinement_of_locallyCompact_sigmaCompact_of_nhds_basis hBU with + ⟨κ, c, W, hW_basis, hW_cover, hW_locallyFinite⟩ + have hκ : Countable κ := by + simpa [Set.countable_univ_iff] using + hW_locallyFinite.countable_univ fun j ↦ ⟨c j, (hW_basis j).2.1⟩ + refine ⟨κ, hκ, ?_⟩ + refine ⟨fun j ↦ ⟨W j, hB.isOpen (hW_basis j).1⟩, ?_, hW_locallyFinite, ?_, ?_⟩ + · exact IsOpenCover.of_sets (fun j ↦ hB.isOpen (hW_basis j).1) hW_cover + · exact fun j ↦ (hW_basis j).1 + · exact fun j ↦ ⟨i (c j), (hW_basis j).2.2⟩ + +/-- **Math.** Theorem 1.15: given an open cover of a topological manifold, there is a +countable locally finite refinement by precompact coordinate balls subordinate to +the cover. **Eng.** Take the countable precompact-coordinate-ball basis from Lemma +1.10, supply the manifold's locally compact + sigma-compact instances (via +`ChartedSpace.locallyCompactSpace` and +`sigmaCompactSpace_of_locallyCompact_secondCountable`), then apply +`exists_countable_locallyFinite_refinement_of_isTopologicalBasis`; each refinement +member lies in the basis, hence is a precompact coordinate ball. -/ +theorem exists_countable_locally_finite_precompact_coordinate_ball_refinement + {ι : Type v} {U : ι → Opens M} (hU : IsOpenCover U) : + ∃ (κ : Type u), Countable κ ∧ ∃ V : κ → Opens M, + IsOpenCover V ∧ LocallyFinite (fun j ↦ (V j : Set M)) ∧ + (∀ j, IsPrecompactCoordinateBall n (V j : Set M)) ∧ + (∀ j, ∃ i, (V j : Set M) ⊆ U i) := by + -- Start from the countable basis of precompact coordinate balls supplied earlier. + have hBasis : + ∃ B : Set (Set M), + B.Countable ∧ IsTopologicalBasis B ∧ ∀ s ∈ B, IsPrecompactCoordinateBall n s := + exists_countable_precompact_coordinate_ball_basis + rcases hBasis with ⟨B, -, hB_basis, hB_precompact⟩ + -- Apply the abstract refinement theorem to this specific basis. + have hRefinement : + ∃ (κ : Type u), Countable κ ∧ ∃ V : κ → Opens M, + IsOpenCover V ∧ LocallyFinite (fun j ↦ (V j : Set M)) ∧ + (∀ j, (V j : Set M) ∈ B) ∧ + (∀ j, ∃ i, (V j : Set M) ⊆ U i) := + by + letI : LocallyCompactSpace M := + ChartedSpace.locallyCompactSpace (EuclideanSpace ℝ (Fin n)) M + letI : SigmaCompactSpace M := sigmaCompactSpace_of_locallyCompact_secondCountable + exact exists_countable_locallyFinite_refinement_of_isTopologicalBasis hU hB_basis + rcases hRefinement with + ⟨κ, hκ, V, hV_cover, hV_locallyFinite, hV_mem, hV_subordinate⟩ + refine ⟨κ, hκ, V, hV_cover, hV_locallyFinite, ?_, hV_subordinate⟩ + intro j + exact hB_precompact _ (hV_mem j) + +end Refinement + +end Manifold From 42f88d931410496670aa1d90dee3c7b82bd55ffc Mon Sep 17 00:00:00 2001 From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com> Date: Sun, 14 Jun 2026 15:05:56 -0400 Subject: [PATCH 2/4] docs(precompact-basis): house-style docstrings Single **Math.** anchor tags (dropped **Eng.** proof-narration), module docstring re-framed by architectural layer (basis needs only topology + chart; refinement adds paracompactness via a reusable abstract lemma), provenance footer. Statements and proofs unchanged. --- .../Manifold/Charts/PrecompactBasis.lean | 83 +++++-------------- 1 file changed, 22 insertions(+), 61 deletions(-) diff --git a/OpenGALib/Manifold/Charts/PrecompactBasis.lean b/OpenGALib/Manifold/Charts/PrecompactBasis.lean index 4ed5f77..2b03792 100644 --- a/OpenGALib/Manifold/Charts/PrecompactBasis.lean +++ b/OpenGALib/Manifold/Charts/PrecompactBasis.lean @@ -11,13 +11,17 @@ import OpenGALib.Manifold.Charts.CoordinateBall /-! # Precompact coordinate balls and locally finite refinements -A *precompact coordinate ball* is the source of a coordinate-ball chart whose -closure is compact. On a topological `n`-manifold — a Hausdorff, second-countable -space charted over `EuclideanSpace ℝ (Fin n)` — these sets form a basis for the -topology, and second countability thins this basis to a countable one (Lee's -Lemma 1.10). Combined with paracompactness, every open cover of such a manifold -admits a countable, locally finite refinement by precompact coordinate balls -subordinate to the cover (Lee's Theorem 1.15). +Covering infrastructure beneath partitions of unity and exhaustions. A +*precompact coordinate ball* is the source of a coordinate-ball chart with +compact closure; on a topological `n`-manifold (Hausdorff, second-countable, +charted over `EuclideanSpace ℝ (Fin n)`) these form a countable basis, and +together with paracompactness every open cover admits a countable, locally +finite refinement by precompact coordinate balls subordinate to it. + +The development is layered: the basis results need only the ambient topology +and a chart; the refinement adds paracompactness, factored through an abstract +basis-refinement lemma (`exists_countable_locallyFinite_refinement_of_isTopologicalBasis`) +reusable for any topological basis. ## Main definitions @@ -32,10 +36,7 @@ subordinate to the cover (Lee's Theorem 1.15). * `Manifold.exists_countable_locally_finite_precompact_coordinate_ball_refinement` — every open cover has a countable locally finite refinement by precompact coordinate balls. -Reference: Lee, *Introduction to Smooth Manifolds*, §1 (Lemma 1.10, Theorem 1.15). - -Ported from SmoothManifoldsLee Chap01/Sec01/Lemma_1_10.lean (a5f308c) -Ported from SmoothManifoldsLee Chap01/Sec01/Theorem_1_15.lean (a5f308c) +Provenance: SmoothManifoldsLee a5f308c — Lemma_1_10, Theorem_1_15. -/ open Set TopologicalSpace @@ -50,25 +51,19 @@ section Basis variable {n : ℕ} {M : Type u} [TopologicalSpace M] /-- **Math.** A set `s ⊆ M` is a *precompact coordinate ball*: it is the source of -some coordinate-ball chart and its closure is compact. **Eng.** Conjunction of an -existential over a chart `e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))` -with `e.source = s` and `e.IsCoordinateBall`, together with -`IsCompact (closure s)`. Stated purely on Mathlib's chart/compactness API. -/ +some coordinate-ball chart and its closure is compact. -/ def IsPrecompactCoordinateBall (n : ℕ) (s : Set M) : Prop := (∃ e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n)), e.source = s ∧ e.IsCoordinateBall) ∧ IsCompact (closure s) -/-- **Math.** A precompact coordinate ball is open. **Eng.** Extract the witnessing -chart `e` with `e.source = s`; the source of an open partial homeomorphism is open -(`e.open_source`), so rewriting along `e.source = s` closes the goal. -/ +/-- **Math.** A precompact coordinate ball is open. -/ theorem IsPrecompactCoordinateBall.isOpen {s : Set M} (hs : IsPrecompactCoordinateBall n s) : IsOpen s := by rcases hs.1 with ⟨e, rfl, -⟩ simpa using e.open_source -/-- **Math.** A precompact coordinate ball has compact closure. **Eng.** Projection -onto the compact-closure component of the defining conjunction. -/ +/-- **Math.** A precompact coordinate ball has compact closure. -/ theorem IsPrecompactCoordinateBall.isCompact_closure {s : Set M} (hs : IsPrecompactCoordinateBall n s) : IsCompact (closure s) := hs.2 @@ -79,14 +74,7 @@ variable [T2Space M] [SecondCountableTopology M] omit [SecondCountableTopology M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] in /-- **Math.** Restricting a chart to a Euclidean open ball whose closed ball is compactly contained in the chart target produces a precompact coordinate ball in -`M`. **Eng.** Restrict `e` to `Metric.ball c r` via `trans (OpenPartialHomeomorph.ofSet …)`; -identify the restricted source/target, get compactness of the closure from the -compact closed ball pushed through the continuous inverse chart, and exhibit the -coordinate-ball witness with `isCoordinateBall_of_target_eq_ball`. The -`[TopologicalManifold n M]` binder of the source is restated as the four Mathlib -classes `[T2Space M] [SecondCountableTopology M] [ChartedSpace … M]`; here only -`[T2Space M]` (for compactness of the closure) is needed beyond the ambient -topology, so the second-countable and charted-space instances are `omit`ted. -/ +`M`. -/ theorem isPrecompactCoordinateBall_chart_preimage_metric_ball (e : OpenPartialHomeomorph M (EuclideanSpace ℝ (Fin n))) {c : EuclideanSpace ℝ (Fin n)} {r : ℝ} (hr : 0 < r) (hclosed : Metric.closedBall c r ⊆ e.target) : @@ -116,11 +104,7 @@ theorem isPrecompactCoordinateBall_chart_preimage_metric_ball omit [SecondCountableTopology M] in /-- **Math.** Every point of an open set lies in a precompact coordinate ball -contained in that open set. **Eng.** Work in the preferred chart `e := chartAt … x`: -its image of `e.source ∩ u` is open, so a small closed Euclidean ball around `e x` -sits inside it; pulling the corresponding open ball back through `e` gives the -required precompact coordinate ball, using -`isPrecompactCoordinateBall_chart_preimage_metric_ball`. -/ +contained in that open set. -/ theorem exists_isPrecompactCoordinateBall_subset_of_mem_open {x : M} {u : Set M} (hx : x ∈ u) (hu : IsOpen u) : ∃ s : Set M, IsPrecompactCoordinateBall n s ∧ x ∈ s ∧ s ⊆ u := by @@ -164,9 +148,7 @@ theorem exists_isPrecompactCoordinateBall_subset_of_mem_open {x : M} omit [SecondCountableTopology M] in /-- **Math.** Precompact coordinate balls form a topological basis on a topological -manifold. **Eng.** Use `isTopologicalBasis_of_isOpen_of_nhds`: each precompact -coordinate ball is open, and `exists_isPrecompactCoordinateBall_subset_of_mem_open` -supplies a basis element inside every open neighborhood of every point. -/ +manifold. -/ theorem isTopologicalBasis_isPrecompactCoordinateBall : IsTopologicalBasis { s : Set M | IsPrecompactCoordinateBall n s } := by -- The local chart construction gives a basis element inside every open neighborhood. @@ -179,10 +161,7 @@ theorem isTopologicalBasis_isPrecompactCoordinateBall : exact ⟨s, hs, hxs, hsu⟩ /-- **Math.** Lemma 1.10: every topological manifold has a *countable* topological -basis consisting of precompact coordinate balls. **Eng.** Start from the (possibly -uncountable) basis `isTopologicalBasis_isPrecompactCoordinateBall`; second -countability lets `IsTopologicalBasis.exists_countable` thin it to a countable -subfamily, every member of which is still a precompact coordinate ball. -/ +basis consisting of precompact coordinate balls. -/ theorem exists_countable_precompact_coordinate_ball_basis : ∃ b : Set (Set M), b.Countable ∧ IsTopologicalBasis b ∧ ∀ s ∈ b, IsPrecompactCoordinateBall n s := by @@ -200,13 +179,7 @@ variable {n : ℕ} {M : Type u} [TopologicalSpace M] [T2Space M] [SecondCountableTopology M] [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] include n in -/-- **Math.** A topological manifold is paracompact. **Eng.** It is locally compact -because charted over the locally compact `EuclideanSpace ℝ (Fin n)` -(`ChartedSpace.locallyCompactSpace`), and second-countable by hypothesis, hence -sigma-compact (`sigmaCompactSpace_of_locallyCompact_secondCountable`); a locally -compact, sigma-compact Hausdorff space is paracompact. The source's -`TopologicalManifold.locallyCompactSpace_of_topologicalManifold` projection is -re-pointed to the Mathlib lemma `ChartedSpace.locallyCompactSpace`. -/ +/-- **Math.** A topological manifold is paracompact. -/ theorem paracompactSpace_of_manifold : ParacompactSpace M := by letI : LocallyCompactSpace M := ChartedSpace.locallyCompactSpace (EuclideanSpace ℝ (Fin n)) M @@ -215,14 +188,7 @@ theorem paracompactSpace_of_manifold : ParacompactSpace M := by /-- **Math.** Companion bridge: given an open cover of a locally compact, sigma-compact, Hausdorff space and any basis for its topology, there is a countable -locally finite refinement by basis elements subordinate to the cover. **Eng.** -Pick, at each point, a cover member containing it; build subordinate neighborhood -bases from `hB` and feed them to Mathlib's -`refinement_of_locallyCompact_sigmaCompact_of_nhds_basis`; local finiteness yields -countability of the index. Placed in `namespace Manifold` (the source put it in the -Mathlib type namespace `TopologicalSpace.IsOpenCover` for `hU.…` dot notation; we -keep the declaration name but state it as a plain theorem to stay inside the -project namespace whitelist — see PR description). -/ +locally finite refinement by basis elements subordinate to the cover. -/ theorem exists_countable_locallyFinite_refinement_of_isTopologicalBasis {X : Type u} [TopologicalSpace X] [LocallyCompactSpace X] [SigmaCompactSpace X] [T2Space X] {ι : Type v} {U : ι → Opens X} @@ -255,12 +221,7 @@ theorem exists_countable_locallyFinite_refinement_of_isTopologicalBasis {X : Typ /-- **Math.** Theorem 1.15: given an open cover of a topological manifold, there is a countable locally finite refinement by precompact coordinate balls subordinate to -the cover. **Eng.** Take the countable precompact-coordinate-ball basis from Lemma -1.10, supply the manifold's locally compact + sigma-compact instances (via -`ChartedSpace.locallyCompactSpace` and -`sigmaCompactSpace_of_locallyCompact_secondCountable`), then apply -`exists_countable_locallyFinite_refinement_of_isTopologicalBasis`; each refinement -member lies in the basis, hence is a precompact coordinate ball. -/ +the cover. -/ theorem exists_countable_locally_finite_precompact_coordinate_ball_refinement {ι : Type v} {U : ι → Opens M} (hU : IsOpenCover U) : ∃ (κ : Type u), Countable κ ∧ ∃ V : κ → Opens M, From 8e98e5a88b248e736cf4c109823873d6e171f7a2 Mon Sep 17 00:00:00 2001 From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com> Date: Sun, 14 Jun 2026 15:07:42 -0400 Subject: [PATCH 3/4] docs(worklist): #66 merged, #67-70 feedback posted --- docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md b/docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md index 80624dc..5a0f06d 100644 --- a/docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md +++ b/docs/log/2026-06-12-smooth-manifolds-lee/WORKLIST.md @@ -115,11 +115,11 @@ strict match to the table above). Actual status takes precedence: | PR | Branch | Content | Status | |---|---|---|---| | #65 | `port/coordinate-ball` | coordinate-ball chart predicates | **merged to develop** (docstrings house-style-revised in db767b1, serves as the exemplar) | -| #66 | `port/precompact-basis` | precompact coordinate-ball countable basis + locally-finite refinement | open, pending feedback: retarget base to develop, revise docstrings | -| #67 | `port/charted-space-core` | manifold from a chart-family core | open, same | -| #68 | `port/exhaustion-cutoff` | exhaustion functions + local smoothness + partition-of-unity ⇒ paracompact | open, same | -| #69 | `port/curve-velocity-mfderiv` | curve velocity + mfderiv (has snake_case defs to rename) | open, same | -| #70 | `port/coordinate-components` | coordinate tangent components (has snake_case defs; inlines `tangent_coordinates_change`) | open, same | +| #66 | `port/precompact-basis` | precompact coordinate-ball countable basis + locally-finite refinement | **merged to develop** (cherry-pick 498d57e, docstrings house-style-revised; second exemplar) | +| #67 | `port/charted-space-core` | manifold from a chart-family core | open, feedback posted | +| #68 | `port/exhaustion-cutoff` | exhaustion functions + local smoothness + partition-of-unity ⇒ paracompact | open, feedback posted | +| #69 | `port/curve-velocity-mfderiv` | curve velocity + mfderiv (has snake_case defs to rename) | open, feedback posted | +| #70 | `port/coordinate-components` | coordinate tangent components (has snake_case defs; inlines `tangent_coordinates_change`) | open, feedback posted | Common feedback (pointing at merged #65 as the exemplar): ① docstring house style (single Math tags / architecture narrative / provenance footer); ② From c60d023a15f6d06b63bf9de33276f60243390ed2 Mon Sep 17 00:00:00 2001 From: Xinze-Li-Moqian <70414198+Xinze-Li-Moqian@users.noreply.github.com> Date: Sun, 14 Jun 2026 15:16:43 -0400 Subject: [PATCH 4/4] =?UTF-8?q?fix(coordinate-ball):=20drop=20unused=20imp?= =?UTF-8?q?ort=20(shake=2039=E2=86=9238)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Mathlib.Geometry.Manifold.ContMDiff.Atlas was unused; shake baseline is 38 and the new domain pushed it to 39, failing CI on the #72 main merge. Carried over from the original port; build + linters unaffected. --- OpenGALib/Manifold/Charts/CoordinateBall.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/OpenGALib/Manifold/Charts/CoordinateBall.lean b/OpenGALib/Manifold/Charts/CoordinateBall.lean index 56de54a..29ef3ef 100644 --- a/OpenGALib/Manifold/Charts/CoordinateBall.lean +++ b/OpenGALib/Manifold/Charts/CoordinateBall.lean @@ -1,6 +1,5 @@ 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