Mathlib v3 is deprecated. Go to Mathlib v4

Theorem continuous_nndist

Modification history

2020-04-02 13:55

src/topology/metric_space/basic.lean

chore(topology/metric_space): use dot notation (#2313) …

Modified continuous_nndist View on Github →

2019-07-03 00:58

src/topology/metric_space/basic.lean

feat(measure_theory): Define Bochner integration (#1149) …

Added continuous_nndist View on Github →