Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-24 19:24 40fa2d84

View on Github →

feat(topology/metric_space): a countably generated uniformity is metrizable (#14052)

Estimated changes

Modified docs/references.bib

Modified src/algebra/group_power/basic.lean

added theorem pow_eq_zero_iff'

Modified src/data/nat/lattice.lean

added theorem nat.Sup_mem

Created src/topology/metric_space/metrizable_uniformity.lean

added theorem pseudo_metric_space.dist_of_prenndist

added theorem pseudo_metric_space.dist_of_prenndist_le

added theorem pseudo_metric_space.le_two_mul_dist_of_prenndist

added theorem uniform_space.metrizable_space