Commit 2021-03-16 16:06 900963cd

refactor(topology/metric_space/emetric_space): add pseudo_emetric (#6694) Working on the Liquid Tensor Experiment, we realize we need seminorms pseudonorms (meaning we don't require ∥x∥ = 0 → x = 0). For this reason I would like to include seminorms, pseudometric and pseudoemetric to mathlib. (We currently have premetric_space, my plan is to change the name to pseudometric_space, that seems to be the standard terminology.) I started modifying emetric_space since it seems the more fundamental (looking at the structure of the imports). What I did here is to define a new class pseudo_emetric_space, generalize almost all the results about emetric_space to this case (I mean, all the results that are actually true) and at the end of the file I defined emetric_space and prove the remaining results. It is the first time I did a refactor like this, so I probably did something wrong, but at least it compiles on my computer. I don't know why one proof in measure_theory/ae_eq_fun_metric.lean stopped working, the same proof in tactic mode works.