mathlib

3798ca1d - feat(topology/metric_space/basic): Distance between constant functions (#16958)

feat(topology/metric_space/basic): Distance between constant functions (#16958) The distance between `λ _, a` and `λ _, b` is at most the distance between `a` and `b`. Also rename `pi_norm_le_iff` to `pi_norm_le_iff_of_nonneg`.