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

[Merged by Bors] - feat(measure_theory/measure/measure_space): The pushfoward measure of a finite measure is a finite measure #9186

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(measure_theory/measure/measure_space): The pushfoward measure of a finite measure is a finite measure #9186

wants to merge 5 commits into from

Conversation

JasonKYi
Copy link
Member

Open in Gitpod

@JasonKYi JasonKYi added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-review The author would like community review of the PR labels Sep 13, 2021
RemyDegenne
RemyDegenne reviewed Sep 13, 2021
View reviewed changes
Copy link
Collaborator

@RemyDegenne RemyDegenne left a comment

Choose a reason for hiding this comment

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

Thanks!

src/measure_theory/measure/measure_space.lean Outdated Show resolved Hide resolved
src/measure_theory/measure/measure_space.lean Outdated Show resolved Hide resolved
@JasonKYi @RemyDegenne
Apply suggestions from code review
abcc028 
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
@RemyDegenne
Copy link
Collaborator

Thanks!
bors r+

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 13, 2021
@RemyDegenne
Copy link
Collaborator

bors r+

bors bot pushed a commit that referenced this pull request Sep 14, 2021
@JasonKYi
feat(measure_theory/measure/measure_space): The pushfoward measure of…
9af1db3 
… a finite measure is a finite measure (#9186)
@bors
Copy link

bors bot commented Sep 14, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory/measure/measure_space): The pushfoward measure of a finite measure is a finite measure [Merged by Bors] - feat(measure_theory/measure/measure_space): The pushfoward measure of a finite measure is a finite measure Sep 14, 2021
@bors bors bot closed this Sep 14, 2021
@bors bors bot deleted the JasonKYi/is_finite_measure_map branch September 14, 2021 08:41
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@RemyDegenne RemyDegenne RemyDegenne left review comments

Assignees
No one assigned
Labels
easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@JasonKYi @RemyDegenne