Mathlib v3 is deprecated. Go to Mathlib v4

Theorem metric.second_countable_of_countable_discretization

Modification history

2019-01-30 09:55
src/topology/metric_space/basic.lean
second countability criteria in metric spaces
Added metric.second_countable_of_countable_discretizationView on Github →