[Merged by Bors] - feat(Order): Fin.orderHom_injective_iff#21119
[Merged by Bors] - feat(Order): Fin.orderHom_injective_iff#21119
Conversation
PR summary de10c3e088Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
|
Thanks very much @mo271 for pointing out the duplicates. I have moved the only new lemma |
Co-authored-by: Moritz Firsching <firsching@google.com>
Mathlib/Order/Fin/Basic.lean
Outdated
| @[simps!] def predAboveOrderHom (p : Fin n) : Fin (n + 1) →o Fin n := | ||
| ⟨p.predAbove, p.predAbove_right_monotone⟩ | ||
|
|
||
| lemma orderHom_injective_iff {α : Type*} [PartialOrder α] {n : ℕ} (f : Fin (n + 1) →o α) : |
There was a problem hiding this comment.
@YaelDillies it looks like this one might have a generalisation in terms of succ orders: do you know if that exists already?
There was a problem hiding this comment.
No it doesn't. It would belong after strictMono_iff_lt_succ
There was a problem hiding this comment.
I have moved the lemma upwards in the file.
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
lgtm now
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
|
Thanks 🎉 bors merge |
This PR adds a lemma `Fin.orderHom_injective_iff` which says that a monotone map `f : Fin (n + 1) →o α` is injective iff `f i.castSucc ≠ f i.succ` for all `i`. Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
This PR adds a lemma
Fin.orderHom_injective_iffwhich says that a monotone mapf : Fin (n + 1) →o αis injective ifff i.castSucc ≠ f i.succfor alli.