[Merged by Bors] - feat(topology/algebra/order/compact): Sup is continuous #13347
Conversation
fpvandoorn
added
the
awaiting-review
| /-- A continuous function is bounded below on a compact set. -/ | ||
| lemma is_compact.bdd_below_image {α : Type u} [topological_space α] [linear_order α] |
There was a problem hiding this comment.
I understand why you put these here, but I think they might be better with the other things related to the extreme value theorem in topology.algebra.order.compact (for example, near is_compact.exists_forall_le). Although this is not a strong preference.
There was a problem hiding this comment.
I can take a look what will break if is_compact.bdd_[below|above] are moved to topology.algebra.order.compact
There was a problem hiding this comment.
In retrospect I think it's probably better to leave those lemmas where they are. They are related to the extreme value theorem, but much weaker, so I think it's fine to put them where they are.
fpvandoorn
added
awaiting-author
fpvandoorn
added
awaiting-review
github-actions
bot
removed
the
awaiting-CI
|
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
Co-authored-by: Johan Commelin <johan@commelin.net>
|
bors merge |
github-actions
bot
added
the
ready-to-merge
* 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
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Supof a binary function over a compact set is continuous in the second variableSupis_compact.bdd_[above|below]_image