[Merged by Bors] - doc(metric): add main results sections for metric spaces#37193
[Merged by Bors] - doc(metric): add main results sections for metric spaces#37193JJYYY-JJY wants to merge 5 commits intoleanprover-community:masterfrom
Conversation
- Summarize the key lemmas and constructions exposed in the metric-space modules to improve discoverability and orientation for readers. - Clarify that many elementary facts live in the pseudo-metric module and update the referenced path accordingly.
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 91b2017b29Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
github-actions
bot
added
the
t-topology
✅ PR Title Formatted CorrectlyThe title of this PR has been updated to match our commit style conventions. |
There was a problem hiding this comment.
Pull request overview
Adds curated “Main results” sections to the pseudo-metric and metric space definition modules to improve discoverability, and updates an implementation note to reference the current pseudo-metric definitions file.
Changes:
- Add “Main results” bullets to
Pseudo/Defs.leanhighlighting key constructions and lemmas. - Add “Main results” bullets to
Defs.leanhighlighting core metric-space constructions and characterizations. - Update the implementation note to point to
Mathlib/Topology/MetricSpace/Pseudo/Defs.lean(removing the stalePseudoMetric.leanreference).
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 1 comment.
| File | Description |
|---|---|
| Mathlib/Topology/MetricSpace/Pseudo/Defs.lean | Adds a “Main results” section listing central pseudo-metric constructions/lemmas. |
| Mathlib/Topology/MetricSpace/Defs.lean | Adds a “Main results” section for metric spaces and fixes an internal file reference in the implementation notes. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
JJYYY-JJY
changed the title
j-loreaux
left a comment
j-loreaux
left a comment
There was a problem hiding this comment.
Thanks for doing this! I think there's some room for further improvement.
j-loreaux
added
the
awaiting-author
- Reorganize "Main definitions" and "Main results" sections in `MetricSpace/Defs.lean` and `MetricSpace/Pseudo/Defs.lean`. - Move `ofDistTopology` and `replace*` functions to the definitions section. - Expand the list of main results for pseudo-metric spaces to include uniformity bases and convergence characterizations.
|
-awaiting-author |
github-actions
bot
removed
the
awaiting-author
Add Main results sections to metric-space definition modules This PR improves discoverability in the metric-space definition modules by adding curated Main results sections and by fixing a stale internal file reference. Add a Main results section to the pseudo-metric definitions module, highlighting key constructions and foundational lemmas. Add a Main results section to the metric-space definitions module, highlighting core constructions and distance-based characterization lemmas. Update the implementation note to point to the current pseudo-metric definitions path, clarifying where elementary pseudometric facts live. This is a docstring-only change: No declarations, theorem names, imports, instances, or proofs are changed; only module docstrings in the two metric-space definition files are edited. Co-authored-by: JJYYY <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Add Main results sections to metric-space definition modules
This PR improves discoverability in the metric-space definition modules by adding curated Main results sections and by fixing a stale internal file reference.
Add a Main results section to the pseudo-metric definitions module, highlighting key constructions and foundational lemmas.
Add a Main results section to the metric-space definitions module, highlighting core constructions and distance-based characterization lemmas.
Update the implementation note to point to the current pseudo-metric definitions path, clarifying where elementary pseudometric facts live.
This is a docstring-only change:
No declarations, theorem names, imports, instances, or proofs are changed;
only module docstrings in the two metric-space definition files are edited.