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] - chore(MeasureTheory): replace continuity -> fun_prop #14008

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore(MeasureTheory): replace continuity -> fun_prop #14008

wants to merge 3 commits into from

Conversation

grunweg
Copy link
Collaborator

@grunweg grunweg commented Jun 20, 2024 •
edited
Loading

Open in Gitpod

@grunweg grunweg added awaiting-review t-measure-probability Measure theory / Probability theory labels Jun 20, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Jun 20, 2024
@grunweg grunweg force-pushed the MR-funprop-measuretheory branch from 1932007 to 712e558 Compare June 24, 2024 14:04
@grunweg grunweg force-pushed the MR-funprop-measuretheory branch from 712e558 to f928b67 Compare June 24, 2024 14:04
@github-actions GitHub Actions
Copy link

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

PR summary 452c1a46e6

Import changes

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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>

@grunweg grunweg removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jun 24, 2024
@j-loreaux
Copy link
Collaborator

bors d+

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 24, 2024

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

@grunweg
Copy link
Collaborator Author

grunweg commented Jun 25, 2024

Thanks for the review.
bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jun 25, 2024
@grunweg
chore(MeasureTheory): replace continuity -> fun_prop (#14008)
cd7c517
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 25, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(MeasureTheory): replace continuity -> fun_prop [Merged by Bors] - chore(MeasureTheory): replace continuity -> fun_prop Jun 25, 2024
@mathlib-bors mathlib-bors bot closed this Jun 25, 2024
@mathlib-bors mathlib-bors bot deleted the MR-funprop-measuretheory branch June 25, 2024 12:07
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@grunweg @kbuzzard
chore(MeasureTheory): replace continuity -> fun_prop (#14008)
116977c
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@grunweg @dagurtomas
chore(MeasureTheory): replace continuity -> fun_prop (#14008)
1af63a3
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@j-loreaux j-loreaux j-loreaux left review comments

Assignees
No one assigned
Labels
delegated t-measure-probability Measure theory / Probability theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@grunweg @j-loreaux @leanprover-community-mathlib4-bot