Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous.edist

Modification history

2021-10-17 11:01
src/topology/instances/ennreal.lean
feat(topology/instances/ennreal): `{f | lipschitz_with K f}` is a closed set (#9766)
Modified continuous.edistView on Github →
2020-04-02 13:55
src/topology/instances/ennreal.lean
chore(topology/metric_space): use dot notation (#2313) …
Added continuous.edistView on Github →