[Merged by Bors] - refactor(topology/metric_space/emetric_space): add pseudo_emetric

[riccardobrasca]

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.

[jcommelin]

Minor point: should the name be pseudo_emetric_space for readability?

[semorrison]

The doc-string on pseudo_emetric_space needs some rewriting to explain the distinction. Also I think the module doc-string should mention pseudo_emetric_space. (A radical proposal would be to actually split into two files.)

[semorrison]

I made two suggestions removing duplicated proofs. Otherwise, LGTM, thank you! Onwards to pseudo_metric_space? :-)

[riccardobrasca]

I improved the docstring.

I don't know about the splitting in two files... Almost everything worked for pseudo_emetric_space (and the rest obviously doesn't work): in practice this will be used as the main emetric_space file 95% of the times.

But how knows, maybe sooner or later someone will need that an extended pseudo metric space is paracompact :)

[semorrison]

bors d+

[bors]

✌️ riccardobrasca can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[riccardobrasca]

bors r+

[bors]

Build failed (retrying...):

• Lint mathlib

[bryangingechen]

I think linting failed on the last commit: https://github.com/leanprover-community/mathlib/runs/2117543193
bors r-

Feel free to put it back on the queue when the linter is happy!

[bors]

Canceled.

[riccardobrasca]

bors r+

[bors]

Build failed (retrying...):

• Build mathlib

[riccardobrasca]

bors r-

[riccardobrasca]

Hmm, it seems I cannot stop bors...

I wanted to do it because working with metric spaces I realized that there is maybe a better strategy for doing this refactor:

• define pseudo_emetric_space as is done now
• have in all the theorems pseudo_emetric_space rather then emetric_space. Of course some of them will not work, and for them add [t2_space]
• define emetric_space as usual, and prove that an Hausdorff pseudo_emetric_space is a emetric_space
• put an instance of emetric_space on an Hausdorff pseudo_emetric_space

The advantage of this is that we will have less duplicate proofs (I believe), for example the product of two emetric_space will be automatically defined by the product of two Hausdorff pseudo_emetric_space.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[riccardobrasca]

I got a lot of deep recursion errors that I don't understand... so I will keep this version for the moment!

[sgouezel]

You can not have both an instance from emetric_space to pseudo_emetric_space, and from pseudo_emetric_space + hausdorff to emetric_space, as this will create a loop. If many lemmas are stated for pseudo_emetric_space and you want to apply them in emetric_space, you definitely need the instance from emetric_space to pseudo_emetric_space, so the other one can only be registered as a def or a lemma, not an instance.

[riccardobrasca]

Ah, you're right!