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(order): add some missing pi
and Prop
instances
#7268
Conversation
urkud
commented
Apr 19, 2021
@@ -926,6 +926,10 @@ lemma supr_subtype' {p : ι → Prop} {f : ∀ i, p i → α} : | |||
(⨆ i (h : p i), f i h) = (⨆ x : subtype p, f x x.property) := | |||
(@supr_subtype _ _ _ p (λ x, f x.val x.property)).symm | |||
|
|||
lemma supr_subtype'' {ι} (s : set ι) (f : ι → α) : |
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.
Perhaps
lemma supr_subtype'' {ι} (s : set ι) (f : ι → α) : | |
lemma supr_coe_subtype {ι} (s : set ι) (f : ι → α) : |
or
lemma supr_subtype'' {ι} (s : set ι) (f : ι → α) : | |
lemma supr_subtype_coe {ι} (s : set ι) (f : ι → α) : |
since (⨆ i : s, f i)
is coercing i
?
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 prefer to separate feature PRs from refactor PRs. Probably we need a PR that uniformizes lemma names for these lemmas and similar lemmas about forall
/exists
/Union
/Inter
.
bors merge |
merge conflict |
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Canceled. |
bors merge |
Timed out. |
bors r+ |
This PR was included in a batch that was canceled, it will be automatically retried |
This PR was included in a batch that was canceled, it will be automatically retried |
This PR was included in a batch that timed out, it will be automatically retried |
Pull request successfully merged into master. Build succeeded: |
pi
and Prop
instancespi
and Prop
instances