[Merged by Bors] - chore: add some fun_prop attributes for continuity
#10769
Conversation
j-loreaux
commented
Feb 20, 2024
j-loreaux
commented
j-loreaux
added
awaiting-review
| @@ -978,6 +978,13 @@ theorem Continuous.comp_continuousOn {g : β → γ} {f : α → β} {s : Set α | |||
| hg.continuousOn.comp hf (mapsTo_univ _ _) | |||
| #align continuous.comp_continuous_on Continuous.comp_continuousOn | |||
|
|
|||
| @[fun_prop] | |||
| theorem Continuous.comp_continuousOn' | |||
There was a problem hiding this comment.
I just realized that fun_prop stores only one composition theorem for each function property. This is true for any lambda theorem (_id,_const,_comp,_pi,_apply). Thus this this theorem clashes with ContinuousOn.comp'' and ContinuousOn.comp'.
The current behavior is that only the latest lambda theorem is used. I think it is ok to keep it marked as fun_prop for now. I will add a support for multiple variants of lambda theorems, I already have this working for fun_trans so it should be quite easy.
|
The rest of the theorems should be fine. |
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
|
✌️ j-loreaux can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-mathlib4-bot
added
delegated
and removed
awaiting-review
Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
|
bors merge |
|
This PR was included in a batch that was canceled, it will be automatically retried |
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
fun_prop attributes for continuityfun_prop attributes for continuity
