# Commit 2021-03-16 16:06 900963cd

View on Github →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.