feat(Topology): Completely Regular Space iff Uniformizable

[plp127]

This PR continues the work from #24096.

Original PR: https://github.com/leanprover-community/mathlib4/pull/24096

---

• [x] depends on: #32140

[github-actions[bot]]

PR summary a73de4ba4b

Import changes for modified files

No significant changes to the import graph M scripts/count-trans-deps.py M scripts/count-trans-deps.py M scripts/count-trans-deps.py

Import changes for all files

Files	Import difference
Mathlib.Topology.UniformSpace.Uniformizable (new file)	1284

---

Declarations diff

+ IsRefl.comp + IsThickening + closure_ball_subset + urysohns_main

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

The privateModule linter not firing is hopefully fixed by #32140: let's wait for that PR to verify the fix here.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#32140~~ By Dependent Issues (🤖). Happy coding!

[j-loreaux]

I don't think this got addressed either:

I just realized we should replace those Prod.mk x ⁻¹' by UniformSpace.ball. We already have UniformSpace.isOpen/Closed_ball.

[j-loreaux]

I would prefer a different name for P above, even though it's private, but Aaron and Junyan disagree with me. I'd like another maintainer to decide.

maintainer merge

[github-actions[bot]]

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

[ocfnash]

Please bring the names in line with the style guide. I appreciate that the guide was written before the module system existed but until it is changed, we should continue to obey it.

[plp127]

Please bring the names in line with the style guide. I appreciate that the guide was written before the module system existed but until it is changed, we should continue to obey it.

I have switched out α for X. Surprisingly, I don't see any part of the naming conventions or style guideline that discourages or forbids my single letter private definition P (and I can't immediately think of what to rename it to). I don't believe urysohns_main is problematic because it is a descriptive name.

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style
• Post-Build Step