Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(analysis/normed_space/basic): define inclusion locally_constant X G → C(X, G) as various types of bundled morphism #8448

Closed
wants to merge 12 commits into from
Closed

[Merged by Bors] - feat(analysis/normed_space/basic): define inclusion locally_constant X G → C(X, G) as various types of bundled morphism #8448

wants to merge 12 commits into from

Conversation

ocfnash
Copy link
Collaborator

@ocfnash ocfnash commented Jul 28, 2021

Open in Gitpod

@ocfnash
feat(analysis/normed_space/basic): define inclusion `locally_constant…
9e41511 
… X G → C(X, G)` as various types of bundled morphism
@ocfnash ocfnash added the awaiting-review The author would like community review of the PR label Jul 28, 2021
ocfnash and others added 2 commits July 28, 2021 15:40
eric-wieser
eric-wieser approved these changes Jul 28, 2021
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

bors d+ (in case you wanted Kevin to look at this first)

@bors
Copy link

bors bot commented Jul 28, 2021

✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 28, 2021
@ocfnash
Copy link
Collaborator Author

ocfnash commented Jul 28, 2021

bors merge

bors bot pushed a commit that referenced this pull request Jul 28, 2021
@ocfnash
feat(analysis/normed_space/basic): define inclusion `locally_constant…
32c8227 
… X G → C(X, G)` as various types of bundled morphism (#8448)
@bors
Copy link

bors bot commented Jul 28, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(analysis/normed_space/basic): define inclusion locally_constant X G → C(X, G) as various types of bundled morphism [Merged by Bors] - feat(analysis/normed_space/basic): define inclusion locally_constant X G → C(X, G) as various types of bundled morphism Jul 28, 2021
@bors bors bot closed this Jul 28, 2021
@bors bors bot deleted the locally_constant_normed_group branch July 28, 2021 18:02
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@eric-wieser eric-wieser eric-wieser approved these changes

@kbuzzard kbuzzard Awaiting requested review from kbuzzard

@laughinggas laughinggas Awaiting requested review from laughinggas

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@ocfnash @eric-wieser