Commit 2022-05-22 23:41 005df456

View on Github →

feat(topology/metric_space): use weaker TC assumptions (#14316) Assume t0_space instead of separated_space in metric.of_t0_pseudo_metric_space and emetric.of_t0_pseudo_emetric_space (both definition used to have t2 in their names).

Estimated changes

Modified src/analysis/normed/group/basic.lean

modified theorem norm_eq_zero_iff'

modified theorem norm_le_zero_iff'

modified theorem norm_pos_iff'

Modified src/topology/metric_space/basic.lean

added theorem metric.indistinguishable_iff

added def metric.of_t0_pseudo_metric_space

deleted def metric.of_t2_pseudo_metric_space

Modified src/topology/metric_space/emetric_space.lean

added theorem emetric.indistinguishable_iff

added def emetric.of_t0_pseudo_emetric_space

deleted def emetric_of_t2_pseudo_emetric_space