Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-30 09:55 ef35c6c3

View on Github →

second countability criteria in metric spaces

Estimated changes

Modified src/topology/continuity.lean

added theorem compact_range

Modified src/topology/metric_space/basic.lean

added theorem metric.second_countable_of_almost_dense_set

added theorem metric.second_countable_of_countable_discretization