Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_map.dist_le

Modification history

2021-04-07 15:23

src/topology/continuous_function/compact.lean

feat(continuous_function/compact): lemmas characterising norm and dist (#7054) …

Added continuous_map.dist_le View on Github →