[Merged by Bors] - feat: continuity of the parametric set integral #11108
Conversation
And copy one necessary variable into the other sections.
grunweg
added
awaiting-review
This changes the order of typeclass arguments; not tried to build all of mathlib yet.
|
Could you please extract a separate mini-PR removing the style exceptions for already-fixed overlong files? (I think two of these are my fault, sorry!) |
|
On the topic of overlong files: we definitely don't want to add new style exceptions if we can help it. I wonder if it might make sense to have a new file called something like |
|
@loefflerd Filed #11137 for the style exceptions. |
grunweg
added
awaiting-review
|
I just realised that I had misunderstood: I thought |
|
I think brutally enforcing |
|
This looks good to me. (Note to maintainers: the issue discussed above about two maintainer merge |
|
🚀 Pull request has been placed on the maintainer queue by loefflerd. |
|
Thank you for the thorough review! |
leanprover-community-mathlib4-bot
added
ready-to-merge
From the sphere eversion project. In passing, we rename variables in one more lemma and use fun_prop in a tiny way.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
…one file (#11139) [Suggested](#11108 (comment)) by @loefflerd. Only code motion (and cosmetic adaptions, such as minimising import and open statements). Pre-requisite for #11108 and (morally) #11110.
See the individual commit messages for details. Extracted from #11108.
From the sphere eversion project. In passing, we rename variables in one more lemma and use fun_prop in a tiny way.
…one file (#11139) [Suggested](#11108 (comment)) by @loefflerd. Only code motion (and cosmetic adaptions, such as minimising import and open statements). Pre-requisite for #11108 and (morally) #11110.
See the individual commit messages for details. Extracted from #11108.
From the sphere eversion project. In passing, we rename variables in one more lemma and use fun_prop in a tiny way.
…one file (#11139) [Suggested](#11108 (comment)) by @loefflerd. Only code motion (and cosmetic adaptions, such as minimising import and open statements). Pre-requisite for #11108 and (morally) #11110.
See the individual commit messages for details. Extracted from #11108.
From the sphere eversion project. In passing, we rename variables in one more lemma and use fun_prop in a tiny way.
…one file (#11139) [Suggested](#11108 (comment)) by @loefflerd. Only code motion (and cosmetic adaptions, such as minimising import and open statements). Pre-requisite for #11108 and (morally) #11110.
See the individual commit messages for details. Extracted from #11108.
From the sphere eversion project. In passing, we rename variables in one more lemma and use fun_prop in a tiny way.
From the sphere eversion project. In passing, we rename variables in one more lemma and use fun_prop in a tiny way.
From the sphere eversion project. In passing, we rename variables in one more lemma and use fun_prop in a tiny way.
From the sphere eversion project.
In passing, we rename variables in one more lemma and use fun_prop in a tiny way.