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

feat: port MeasureTheory.Constructions.Prod.Basic #4168

Closed
wants to merge 105 commits into from
Closed

feat: port MeasureTheory.Constructions.Prod.Basic #4168

wants to merge 105 commits into from

Conversation

Komyyy
Copy link
Collaborator

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

Komyyy and others added 30 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.Function.SimpleFunc
ed7779c
@Komyyy
Initial file copy from mathport
4e5490c
@Komyyy
automated fixes
938c1ec 
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…
51ac57a 
… port/MeasureTheory.Function.SimpleFunc
@Komyyy
fix
aef6c9e
@Komyyy
fix
3c000d0
@Komyyy
fix
07f611a
@Komyyy
feat: port MeasureTheory.Integral.Lebesgue
b5a8222
@Komyyy
Initial file copy from mathport
18e3037
@Komyyy
automated fixes
464a1de 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@Komyyy
Merge branch 'port/MeasureTheory.Function.SimpleFunc' into port/Measu…
ade1261 
…reTheory.Integral.Lebesgue
@Komyyy Komyyy added awaiting-CI and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels May 25, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 26, 2023
@Komyyy Komyyy removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 26, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 26, 2023
@kim-em
Copy link
Contributor

kim-em commented May 27, 2023

Is it necessary to have this stacked on top of #4200? It would be nice if these could proceed independently.

@Komyyy Komyyy closed this May 28, 2023
@Komyyy Komyyy deleted the port/MeasureTheory.Constructions.Prod.Basic branch May 28, 2023 02:31
@Komyyy
Copy link
Collaborator Author

Komyyy commented May 28, 2023

@semorrison The new PR is #4433.

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
blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) mathlib-port This is a port of a theory file from mathlib. merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
6 participants
@Komyyy @kim-em @urkud @ChrisHughes24 @Parcly-Taxel @kmill