-
Notifications
You must be signed in to change notification settings - Fork 298
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/rel_iso): well_founded (quotient.lift₂ r H) ↔ well_founded r
#15890
Conversation
vihdzp
commented
Aug 6, 2022
•
edited
edited
- depends on: [Merged by Bors] - perf(number_theory/padics/hensel): squeeze simps #15926
well_founded (quotient.lift₂ r H)
→ well_founded r
well_founded (quotient.lift₂ r H) → well_founded r
well_founded (quotient.lift₂ r H) → well_founded r
well_founded (quotient.lift₂ r H) ↔ well_founded r
/-- A relation is well founded iff its lift to a quotient is. -/ | ||
@[simp] theorem _root_.well_founded_lift₂_iff [s : setoid α] {r : α → α → Prop} | ||
(H : ∀ a₁ a₂ b₁ b₂ : α, a₁ ≈ b₁ → a₂ ≈ b₂ → r a₁ a₂ = r b₁ b₂) : | ||
well_founded (quotient.lift₂ r H) ↔ well_founded r := |
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.
You might want one for quotient.lift_on₂' r H
too, which is trivial to prove.
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.
quotient.lift_on₂'
is reducible and def-eq to quotient.lift_on₂
, which itself is reducible and def-eq to quotient.lift₂
. So I think just having this last version should be enough.
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.
Can you verify that simp
can prove the primed version by itself?
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.
It can. And now that I think about it, λ x y, quotient.lift_on₂' x y r H
is a very awkward spelling for quotient.lift₂ r H
, so I doubt this will come up in practice.
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.
quotient.lift_on₂'
is useful for when the setoid is not an instance, which is quite common. But if simp
doesn't need the lemma about it here, then there's probably no issue.
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.
bors d+
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
This avoids a timeout in #15890.
Did you mean to mark this as depending on itself? |
That was a mistake, fixed. |
This PR/issue depends on:
|
bors r+ |
Pull request successfully merged into master. Build succeeded: |
well_founded (quotient.lift₂ r H) ↔ well_founded r
well_founded (quotient.lift₂ r H) ↔ well_founded r