[Merged by Bors] - feat(data/fin/tuple/basic): injectivity of fin.cons x xs
#17779
Conversation
eric-wieser
commented
Dec 1, 2022
eric-wieser
commented
eric-wieser
added
the
awaiting-review
| @@ -301,8 +301,21 @@ theorem of_fn_eq_map {α n} {f : fin n → α} : | |||
| of_fn f = (fin_range n).map f := | |||
| by rw [← of_fn_id, map_of_fn, function.right_id] | |||
|
|
|||
| theorem nodup_of_fn {α n} {f : fin n → α} (hf : function.injective f) : | |||
| theorem nodup_of_fn_of_injective {α n} {f : fin n → α} (hf : function.injective f) : | |||
There was a problem hiding this comment.
It's unfortunate that of_fn has a name like that, it makes all the names involving it hard to read. I'm thinking perhaps dot notation might be a nice way around it:
| theorem nodup_of_fn_of_injective {α n} {f : fin n → α} (hf : function.injective f) : | |
| theorem _root_.function.injective.nodup_of_fn {α n} {f : fin n → α} (hf : function.injective f) : |
There was a problem hiding this comment.
I don't really like moving this out of the list namespace, because neither nodup or of_fn are immediately recognizable as list operators.
There was a problem hiding this comment.
I could just inline this into nodup_of_fn if the name is really unlikable; it's not needed once the iff is available.
There was a problem hiding this comment.
It's fine to keep the current name, I just would like to encourage you to think of an alternative :)
There was a problem hiding this comment.
How about (in a future PR) renaming list.of_fn to fin.to_list or function.to_list or tuple.to_list?
| | 0 x := by convert h0 | ||
| | (n + 1) x := cons_cases (λ x₀ x, h _ _ $ cons_induction _) x | ||
|
|
||
| lemma cons_injective_of_injective {α} {x₀ : α} {x : fin n → α} (hx₀ : x₀ ∉ set.range x) |
There was a problem hiding this comment.
I don't mind this name so much, this suggestion is more to match with the nodup_of_fn suggestion:
| lemma cons_injective_of_injective {α} {x₀ : α} {x : fin n → α} (hx₀ : x₀ ∉ set.range x) | |
| lemma _root_.function.injective.fin_cons {α} {x₀ : α} {x : fin n → α} (hx₀ : x₀ ∉ set.range x) |
|
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
leanprover-community-bot-assistant
added
delegated
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
jcommelin
added
the
awaiting-author
|
bors merge |
github-actions
bot
added
ready-to-merge
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
fin.cons x xsfin.cons x xs
