mathlib

adfe9c7f - feat(topology/algebra/order/compact): Sup is continuous (#13347)

feat(topology/algebra/order/compact): Sup is continuous (#13347) * Prove that the `Sup` of a binary function over a compact set is continuous in the second variable * Some other lemmas about `Sup` * Move and generalize `is_compact.bdd_[above|below]_image` * from the sphere eversion project