mathlib

8459d0a6 - feat(continuous_function/compact): lemmas characterising norm and dist (#7054)

feat(continuous_function/compact): lemmas characterising norm and dist (#7054) Transport lemmas charactering the norm and distance on bounded continuous functions, to continuous maps with compact domain. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>