New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor(topology/bounded_continuous_function): structure extending continuous_map #6521
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This looks good to me! Let's make sure @sgouezel sees this, he wrote the file, and my impression that this was a desirable refactor also came from him.
I am mildly in favour of renaming continuous_map
to continuous_function
-- it's a shame because continuous_map
is more idiomatic, but I think consistency is more important.
Why not go to |
The primary use of the file is "bounded continuous function" / "bounded continuous functions", 107k + 99k Google hits |
ok, I don't know the literature, so I retract my suggestion |
Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
bors merge |
…ontinuous_map (#6521) Convert `bounded_continuous_function` from a subtype to a structure extending `continuous_map`, and some minor improvements to `@[simp]` lemmas. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed: |
bors merge |
…ontinuous_map (#6521) Convert `bounded_continuous_function` from a subtype to a structure extending `continuous_map`, and some minor improvements to `@[simp]` lemmas. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
…ontinuous_map (#6521) Convert `bounded_continuous_function` from a subtype to a structure extending `continuous_map`, and some minor improvements to `@[simp]` lemmas. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
…ontinuous_map (#6521) Convert `bounded_continuous_function` from a subtype to a structure extending `continuous_map`, and some minor improvements to `@[simp]` lemmas. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Convert
bounded_continuous_function
from a subtype to a structure extendingcontinuous_map
, and some minor improvements to@[simp]
lemmas.A question: should I rename
continuous_map
tocontinuous_function
, for uniformity? I'm inclined to.