Commit 2026-08-25 01:15 ce084ccd

View on Github →

feat(Topology/MetricSpace): add distance congruence lemmas (#42893)

Estimated changes

modified theorem SeparationQuotient.dist_mk
added theorem dist_congr
added theorem dist_congr_left
added theorem dist_congr_right
added theorem nndist_congr
added theorem nndist_congr_left
added theorem nndist_congr_right