Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-16 07:16 6a09cd06

View on Github →

chore(topology/uniform_space): use weaker TC assumptions (#12066) We don't need [uniform_space β] to prove uniform_space.completion.ext.

Estimated changes

Modified src/topology/uniform_space/abstract_completion.lean

Modified src/topology/uniform_space/completion.lean

modified theorem uniform_space.completion.ext