mathlib

mathlib copied to clipboard

• Remove the t2_space assumption from exists_compact_between by generalizing the proof of exists_compact_superset, and move it from topology/separation to topology/subset_properties.
• Use it to prove continuous_map.continuous_prod in topology/continuous_map stating that for topological spaces X,Y,Z with Y locally compact, the composition induces a continuous map from C(X,Y) x C(Y,Z) to C(X,Z) where all function spaces are endowed with the compact-open topology. The (statement and the) proof is taken from Prop. 9 of Chap. X, §3, №. 4 of Bourbaki's Topologie Générale.
• Generalize exists_open_between_and_is_compact_closure from t3_space to t2_space using the generalized exists_compact_between.

This has been briefly discussed in this Zulip discussion

With your exists_compact_superset' you can now remove exists_compact_between which has the extraneous t3_space assumption. The same assumption could be removed from exists_open_between_and_is_compact_closure as well, but this lemma seems not used at all in mathlib.

Oh, nice! Thanks for pointing this out. I will work on these lemmas tomorrow and will push a new version of the PR.

Oh sorry, I now realize t3_space can't be totally removed from exists_open_between_and_is_compact_closure, but it can be replaced by t2_space given your lemma; as soon as you want the closure of a compact set to be compact, you need separation axioms. So I think all you need to do is to rename your exists_compact_superset' to exists_compact_between, and move exists_open_between_and_is_compact_closure up to the section of t2_space lemmas.

I've been able to adapt the proof of exists_compact_superset to more easily prove exists_compact_between, and then exists_compact_superset becomes a trivial consequence. Feel free to merge! (Update: I've also golfed continuous_prod in that branch by now.)

Ok, thanks, but now I am lost. What should I do?

I've basically done all the things I mentioned above in that branch, so you can just merge it and then I think this PR is good to go. If you have trouble merging I can also directly push to this PR.

Yes, I have seen that branch and it looks very good to me, but I would find it easier if you could rather suggest edits to this one, that I will all commit, so we avoid duplicates (I find it harder to follow what goes on). Thanks!

This link is the diff between the branches but I agree the diff is a bit large, mainly because some lemmas are moved; but you can also check individual commits there. https://github.com/leanprover-community/mathlib/compare/fae_curry_C_locally_compact...curry_locally_compact

Ok, I think I have merged the other branch to this one. Right?

Yes, it appears to be a squash merge. Thanks!

It's interesting that you opened another PR on github and merged it to a nonmaster branch, instead of doing it locally. I never tried it and it's nice to know that bors still takes care of such PR, squash merges it and deletes the merged branch. Thanks for testing it out!

I actually still see the old branch on the list of PR's (although it appears as a merged one), have you seen it disappear? Or maybe the PR is still there but the branch disappeared?

Yes the branch is deleted but the PR is still there (check the bottom of the PR for the deletion message; good hygiene automated by bors!).

I'll update the PR title/description since only one new lemma is added.

I'll update the PR title/description since only one new lemma is added.

Sure! I have updated co-authorship (but please emend this if you so wish, in case of errors).

Actually bors will add my name because of my commits in the merged branch; so we'd better remove the coauthor message to avoid duplication.

Actually bors will add my name because of my commits in the merged branch; so we'd better remove the coauthor message to avoid duplication.

Ah, ops, did not know - done!

Actually bors will add my name because of my commits in the merged branch

You can see that already happened in the squashed merge commit: https://github.com/leanprover-community/mathlib/pull/15721/commits/06d609d486920e3ac964fa4a8ab59dca40eae73b

Thanks!

bors merge

Pull request successfully merged into master.

Build succeeded:

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