-
Notifications
You must be signed in to change notification settings - Fork 235
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.
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
[Merged by Bors] - feat: MeasureSpace
instance on unitInterval
#10452
Conversation
/-- `unitInterval.symm` as a `MeasurableEquiv`. -/ | ||
@[simps] | ||
def symmMeasurableEquiv : I ≃ᵐ I := symmHomeomorph.toMeasurableEquiv |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@urkud, do you think this is worth having, or should I delete it?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would remove it as it's so easy to access it from the homeomorphism.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩ | ||
theorem symm_involutive : Function.Involutive (symm : I → I) := symm_symm | ||
|
||
theorem symm_bijective : Function.Bijective (symm : I → I) := symm_involutive.bijective |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do you mind adding deprecated aliases for old names (involutive_symm
and bijective_symm
below)? Otherwise LGTM. Thanks!
bors d+
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Done
bors merge
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
Also shows that it is a probability measure, and that `symm` is measurable. This deprecates two duplicate theorems. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/MeasureSpace.20instance.20on.20unitInterval/near/420921313)
This PR was included in a batch that was canceled, it will be automatically retried |
Also shows that it is a probability measure, and that `symm` is measurable. This deprecates two duplicate theorems. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/MeasureSpace.20instance.20on.20unitInterval/near/420921313)
Pull request successfully merged into master. Build succeeded: |
MeasureSpace
instance on unitInterval
MeasureSpace
instance on unitInterval
Also shows that it is a probability measure, and that `symm` is measurable. This deprecates two duplicate theorems. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/MeasureSpace.20instance.20on.20unitInterval/near/420921313)
Also shows that it is a probability measure, and that `symm` is measurable. This deprecates two duplicate theorems. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/MeasureSpace.20instance.20on.20unitInterval/near/420921313)
Also shows that it is a probability measure, and that `symm` is measurable. This deprecates two duplicate theorems. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/MeasureSpace.20instance.20on.20unitInterval/near/420921313)
Also shows that it is a probability measure, and that `symm` is measurable. This deprecates two duplicate theorems. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/MeasureSpace.20instance.20on.20unitInterval/near/420921313)
Also shows that it is a probability measure, and that
symm
is measurable.This deprecates two duplicate theorems.
Zulip