Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-17 03:47 d292fd7e

View on Github →

refactor(topology/metric_space/basic): add pseudo_metric (#6716) This is the natural continuation of #6694: we introduce here pseudo_metric_space. Note that I didn't do anything fancy, I only generalize the results that work out of the box for pseudometric spaces (quite a lot indeed). It's possible that there is some duplicate code, especially in the section about products.

Estimated changes

modified theorem ball_prod_same
modified theorem closed_ball_prod_same
modified theorem dist_comm
modified theorem dist_eq_zero
modified theorem dist_le_zero
modified theorem dist_pos
modified theorem dist_self
modified theorem edist_lt_top
modified theorem eq_of_dist_eq_zero
modified theorem eq_of_forall_dist_le
modified theorem eq_of_nndist_eq_zero
modified theorem metric.continuous_at_iff
modified theorem metric.continuous_iff
modified theorem metric.continuous_on_iff
modified theorem metric.mem_closure_iff
modified theorem metric.mem_of_closed'
modified theorem metric.tendsto_nhds_nhds
modified def metric_space.induced
modified theorem nndist_eq_zero
modified theorem nndist_pi_const
modified theorem prod.dist_eq
added theorem subtype.pseudo_dist_eq
modified theorem zero_eq_dist
modified theorem zero_eq_nndist
added theorem pseudo_edist_pi_const
added theorem pseudo_edist_pi_def
deleted theorem pseudoedist_pi_const
deleted theorem pseudoedist_pi_def
modified def metric.glue_premetric