Mathlib Changelog
v4
Changelog
About
Github
Theorem
nndist_congr
Modification history
2026-08-25 01:15
Mathlib/Topology/MetricSpace/Basic.lean
feat(Topology/MetricSpace): add distance congruence lemmas (#42893)
Added
nndist_congr
View on Github →