Commit 2025-12-18 14:20 5233f83e

View on Github →

feat(Topology): Completely Regular Space iff Uniformizable (#32080) This PR continues the work from #24096. Original PR: https://github.com/leanprover-community/mathlib4/pull/24096

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Rel.lean

Modified Mathlib/Topology/UniformSpace/Basic.lean

added theorem closure_ball_subset

Created Mathlib/Topology/UniformSpace/Uniformizable.lean

added def IsThickening

added theorem urysohns_main