[Merged by Bors] - feat(Mathlib.Topology.Compactness.Compact): add sInter version of Cantor's intersection theorem

[oliver-butterley]

The iInter version of Cantor's intersection theorem is already present: IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed.
The proof of the added sInter version takes advantage of the iInter version.

Much of the addition due to conversation with Sebastien Gouezel on Zulip.

[oliver-butterley]

I believe that:
IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed
would be the recommended naming scheme. However the chosen name:
IsCompact.nonempty_sInter_of_directed_nonempty_compact_closed
matches the other results in the same file.

[oliver-butterley]

Maybe it help reviewers if I link to the place where the added theorem is used?
It is used in topology.lean in this branch of this project: [https://github.com/oliver-butterley/birkhoff/tree/wip-exist-minimal]

[sgouezel]

bors r+
Thanks!

[sgouezel]

bors r-

[mathlib-bors]

Canceled.

[sgouezel]

Suggested change

	theorem IsCompact.nonempty_sInter_of_directed_nonempty_compact_closed
	theorem IsCompact.nonempty_sInter_of_directed_nonempty_isCompact_isClosed

We try to have theorem names that follow as closely as possible the Lean names. The other IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed is also wrong, by the way -- could you correct it, and add a deprecated alias for the old name? (If you don't know how to do that, tell me)

[oliver-butterley]

Sure thing, I've corrected the name of the newly added theorem.

I've updated the naming of the other two cantor intersection theorems and added the alias. Shall I do this as part of this PR or better as a separate PR? I've done them here but let me know and I can revert this and do a separate PR for the name change.

The mathlib style guide doesn't tell me the preferred place for the deprecated alias. Sometimes they are the end of the files and sometimes they are immediately after the associated theorem. I've put it after the theorem with a single space between the two since there is already the #align there. Otherwise at the end of the file seems more tidy to me. Give me guidance and then I can change is (and also add a note to the style guide if there is a maintainer consensus.)

[sgouezel]

Looks great. Can you just add the deprecation date before the aliases, so that we can remove them in due time. And also fix the long line, and replace the uses of deprecated theorems by the non-deprecated ones? (There should be a code action, i.e., a blue light bulb that shows up when you click on the deprecated use, suggesting the right replacement).

[oliver-butterley]

I did the changes to all the uses of the theorem and added the dates.

[sgouezel]

bors r+
Thanks!

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style