Skip to content

[Merged by Bors] - chore: Split large file MeasureTheory.MeasurableSpace.Basic#13937

Closed
loefflerd wants to merge 2 commits intomasterfrom
DL_split_measurablespace
Closed

[Merged by Bors] - chore: Split large file MeasureTheory.MeasurableSpace.Basic#13937
loefflerd wants to merge 2 commits intomasterfrom
DL_split_measurablespace

Conversation

@loefflerd
Copy link
Copy Markdown
Contributor

@loefflerd loefflerd commented Jun 18, 2024

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 18, 2024 •
edited
Loading

PR summary e7c0539f2a

Import changes

No significant changes to the import graph

Declarations diff

+-+- measurableSet_image

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@loefflerd loefflerd requested a review from YaelDillies June 18, 2024 20:17
@loefflerd loefflerd mentioned this pull request Jun 18, 2024
Closed
4 tasks
grunweg
grunweg approved these changes Jun 18, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

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

Thanks a lot for doing this. Splitting large files is a tedious task, but very important in the long term. The split you have found makes sense to me.

Can I ask for one more thing, namely extending the module docstring of MeasurableSpace/Embedding.lean a bit, to mention its main results? I could be convinced that refl, symm, trans, products etc., are standard and can be omitted - but the measurable Schröder-Bernstein theorem definitely seems worth mentioning.

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jun 18, 2024

awaiting-author

@github-actions github-actions bot added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 18, 2024
@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jun 18, 2024

I just saw you asked for Yael's opinion - well, now you have mine as well. Hope it's helpful :-)

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jun 18, 2024

(And this PR needs small shaking of imports.)

@YaelDillies YaelDillies changed the title Split large file Mathlib/MeasureTheory/MeasurableSpace/Basic.lean chore: Split large file MeasureTheory.MeasurableSpace.Basic Jun 18, 2024
@loefflerd loefflerd added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 19, 2024
@loefflerd
Copy link
Copy Markdown
Contributor Author

loefflerd commented Jun 19, 2024

Thanks for the review Michael! I asked Yael for a review initially since he was already reviewing #13353, but your input is also very welcome. I have adjusted the imports and added a fuller docstring as you suggested.

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Jun 19, 2024

Thanks for these changes; this split looks good to me now!
Let me approve already - if Yael has strong opinions, the split can always be tweaked later.
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 19, 2024

🚀 Pull request has been placed on the maintainer queue by grunweg.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 19, 2024
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Jun 19, 2024

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 19, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 19, 2024
@loefflerd
chore: Split large file MeasureTheory.MeasurableSpace.Basic (#13937)
572940c
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: Split large file MeasureTheory.MeasurableSpace.Basic [Merged by Bors] - chore: Split large file MeasureTheory.MeasurableSpace.Basic Jun 19, 2024
@mathlib-bors mathlib-bors bot closed this Jun 19, 2024
@mathlib-bors mathlib-bors bot deleted the DL_split_measurablespace branch June 19, 2024 10:33
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@loefflerd @AntoineChambert-Loir
chore: Split large file MeasureTheory.MeasurableSpace.Basic (#13937)
d30c127
grunweg pushed a commit that referenced this pull request Jun 20, 2024
@loefflerd @grunweg
chore: Split large file MeasureTheory.MeasurableSpace.Basic (#13937)
a2e3987
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@loefflerd @kbuzzard
chore: Split large file MeasureTheory.MeasurableSpace.Basic (#13937)
65cdd90
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@grunweg grunweg grunweg approved these changes

@YaelDillies YaelDillies Awaiting requested review from YaelDillies

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@loefflerd @grunweg @jcommelin