mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(topology/metric_space/basic): Distance between constant functions

Open YaelDillies opened this issue 3 years ago • 0 comments

The distance between λ _, a and λ _, b is less than the distance between a and b.

Open in Gitpod

YaelDillies avatar Oct 13 '22 18:10 YaelDillies