Skip to content
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] - feat(measure_theory/measure/measure_space): A measurable_equiv is quasi_measure_preserving #17774

Closed
wants to merge 4 commits into from

Conversation

YaelDillies
Copy link
Collaborator


Open in Gitpod

@YaelDillies YaelDillies requested a review from a team as a code owner November 30, 2022 17:29
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR easy < 20s of review time. See the lifecycle page for guidelines. t-measure-probability Measure theory / Probability theory labels Nov 30, 2022
Copy link
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

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

This should be something like measurable_equiv.quasi_measure_preserving_symm or measurable_equiv.quasi_measure_preserving_symm_map. Could you also prove the analogue for measure_preserving?

@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed easy < 20s of review time. See the lifecycle page for guidelines. awaiting-review The author would like community review of the PR labels Dec 1, 2022
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 13, 2022
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 16, 2022
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Dec 16, 2022
@sgouezel
Copy link
Collaborator

bors d+
Thanks!

@bors
Copy link

bors bot commented Dec 16, 2022

✌️ YaelDillies 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 Dec 16, 2022
@YaelDillies
Copy link
Collaborator Author

Great!

bors merge

bors bot pushed a commit that referenced this pull request Dec 16, 2022
@bors
Copy link

bors bot commented Dec 16, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(measure_theory/measure/measure_space): A measurable_equiv is quasi_measure_preserving [Merged by Bors] - feat(measure_theory/measure/measure_space): A measurable_equiv is quasi_measure_preserving Dec 16, 2022
@bors bors bot closed this Dec 16, 2022
@bors bors bot deleted the quasi_measure_preserving_map branch December 16, 2022 16:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated The PR author may merge after reviewing final suggestions. t-measure-probability Measure theory / Probability theory
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants