min and max are continuous

[zstone1]

Another quick, but missing, foundational topology result. The functions min, max : T * T -> T are continuous. There are a couple inelegant things about the proofs. Firstly, I end up having to case on whether x : T has an immediate successor or not. Annoying, but fine. I end up proving both min and max by hand. Ideally I'd prove one, and then the other would follow by flipping the inequalities. But there doesn't seem to be a mathcomp constructor for the "opposite" order, which is what I would need.

Neither of these annoyances should be blockers

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

I just performed a linting phase and gain a dozen of lines.