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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: port MeasureTheory.Constructions.Polish #4064

Closed
wants to merge 47 commits into from
Closed

[Merged by Bors] - feat: port MeasureTheory.Constructions.Polish #4064

wants to merge 47 commits into from

Conversation

Komyyy
Copy link
Collaborator

@Komyyy Komyyy commented May 18, 2023 •
edited by github-actions bot

Komyyy and others added 24 commits May 16, 2023 12:35
@Komyyy
feat: port MeasureTheory.Constructions.BorelSpace.Basic
0b718b0
@Komyyy
Initial file copy from mathport
9d3c729
@Komyyy
automated fixes
997cdc6 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Komyyy
fix
c862990
@Komyyy
fix
ce2555b
@urkud
Fix imports
077a467
@urkud
Fix more
09be11b
@urkud
Fix more
9f825b6
@Komyyy
borelize
fe8ffb0
@Komyyy
borelize
9d88ac7
@Komyyy
Merge branch 'master' into port/MeasureTheory.Constructions.BorelSpac…
b501d57 
…e.Basic
@Komyyy
fix
7e488be
@Komyyy
fix
5403d20
@Komyyy
Merge branch 'Filter.iInf_isMeasurablyGenerated' into port/MeasureThe…
1701692 
…ory.Constructions.BorelSpace.Basic
@Komyyy
fix
4d0942c
@Komyyy
fix
d0617a2
@Komyyy
borelize
c579ecc
@Komyyy
fix
d8d4166
@Komyyy
fix
b9f174c
@Komyyy
feat: port MeasureTheory.Constructions.Polish
d87137a
@Komyyy
Initial file copy from mathport
6980a13
@Komyyy
automated fixes
4230e64 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Komyyy
Merge branch 'port/MeasureTheory.Constructions.BorelSpace.Basic' into…
09a0183 
… port/MeasureTheory.Constructions.Polish
@Komyyy
fix
e38fde5
@Komyyy Komyyy added blocked-by-math-PR This PR depends on another PR to Mathlib awaiting-review The author would like community review of the PR mathlib-port This is a port of a theory file from mathlib. awaiting-CI labels May 18, 2023
@Komyyy Komyyy removed the blocked-by-math-PR This PR depends on another PR to Mathlib label May 21, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label May 21, 2023
@Komyyy Komyyy added awaiting-CI and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels May 21, 2023
@ChrisHughes24
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels May 21, 2023
@bors
Copy link

bors bot commented May 21, 2023

Merge conflict.

@ChrisHughes24
Copy link
Member

bors merge

@ChrisHughes24
Copy link
Member

bors r-
bors d+

@bors
Copy link

bors bot commented May 21, 2023

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

@bors
Copy link

bors bot commented May 21, 2023

Canceled.

@ChrisHughes24
Copy link
Member

bors merge

@bors
Copy link

bors bot commented May 21, 2023

Canceled.

@ChrisHughes24
Copy link
Member

bors merge

bors bot pushed a commit that referenced this pull request May 21, 2023
@Komyyy @Parcly-Taxel
@ChrisHughes24 @urkud
feat: port MeasureTheory.Constructions.Polish (#4064)
9646956 
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
@bors
Copy link

bors bot commented May 21, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: port MeasureTheory.Constructions.Polish [Merged by Bors] - feat: port MeasureTheory.Constructions.Polish May 21, 2023
@bors bors bot closed this May 21, 2023
@bors bors bot deleted the port/MeasureTheory.Constructions.Polish branch May 21, 2023 16:45
qawbecrdtey pushed a commit to qawbecrdtey/greedoid-mathlib4 that referenced this pull request Jun 12, 2023
@Komyyy @Parcly-Taxel
@ChrisHughes24 @urkud @qawbecrdtey
feat: port MeasureTheory.Constructions.Polish (leanprover-community#4064
b7e978e 
)

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Chris Hughes <chrishughes24@gmail.com>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
delegated mathlib-port This is a port of a theory file from mathlib. 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.

None yet
5 participants
@Komyyy @semorrison @ChrisHughes24 @urkud @Parcly-Taxel