[Merged by Bors] - feat: some measure preserving equivalences on pi-types#7751
[Merged by Bors] - feat: some measure preserving equivalences on pi-types#7751fpvandoorn wants to merge 3 commits intomasterfrom
Conversation
| #align measure_theory.volume_preserving_pi_equiv_pi_subtype_prod MeasureTheory.volume_preserving_piEquivPiSubtypeProd | ||
|
|
||
| theorem measurePreserving_piCongrLeft (f : ι' ≃ ι) : | ||
| MeasurePreserving (MeasurableEquiv.piCongrLeft α f) |
There was a problem hiding this comment.
Out of scope for this PR, since you're following the existing pattern, but... Shouldn't this be stated in the less-bundled way as:
| MeasurePreserving (MeasurableEquiv.piCongrLeft α f) | |
| MeasurePreserving (Equiv.piCongrLeft α f) |
There was a problem hiding this comment.
I'm not sure. I want to use both the MeasurableEquiv and MeasurePreserving parts at the same time when applying this theorem:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/Lebesgue.html#MeasureTheory.MeasurePreserving.lintegral_map_equiv
That is easier to apply if this is formulated using MeasurableEquiv.
|
✌️ fpvandoorn can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
* Also fix the statement of some lemmas of an earlier PR. * From the Sobolev project * There are more that depend on #7341 Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com
|
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. If you want to switch to GitHub's built-in merge queue, visit their help page. |
updateFinsetwhich updates a finite number components of a vector #7341Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com