[Merged by Bors] - refactor(data/set/finite): change type of set.finite.dependent_image
#6475
Conversation
The old lemma combined a statement similar to `set.finite.image` with `set.finite.subset`. The new statement is a direct generalization of `set.finite.image`.
src/data/set/finite.lean
Outdated
| lemma finite.dependent_image {s : set α} (hs : finite s) {F : Π i ∈ s, β} {t : set β} | ||
| (H : ∀ y ∈ t, ∃ x (hx : x ∈ s), y = F x hx) : set.finite t := | ||
| lemma finite.dependent_image {s : set α} (hs : finite s) (F : Π i ∈ s, β) : | ||
| finite {y : β | ∃ x (hx : x ∈ s), F x hx = y} := |
There was a problem hiding this comment.
Why did you change the order here? I mean, go from y = F x hx to F x hx = y? Typically, in applications if you rcase along this you will get an assumption h : y = F x hx along which you can rewrite directly, while if you get F x hx = y you will have to rewrite in the reverse direction, which seems less natural.
There was a problem hiding this comment.
My goal was to match the definition of set.image but I can revert this part (or drop the whole PR - it turns out that I won't need it).
There was a problem hiding this comment.
I don't mind the PR, but I really prefer the other direction.
| @@ -573,7 +573,7 @@ def comp_partial_sum_target_set (m M N : ℕ) : set (Σ n, composition n) := | |||
|
|
|||
| lemma comp_partial_sum_target_subset_image_comp_partial_sum_source | |||
| (m M N : ℕ) (i : Σ n, composition n) (hi : i ∈ comp_partial_sum_target_set m M N) : | |||
| ∃ j (hj : j ∈ comp_partial_sum_source m M N), i = comp_change_of_variables m M N j hj := | |||
| ∃ j (hj : j ∈ comp_partial_sum_source m M N), comp_change_of_variables m M N j hj = i := | |||
There was a problem hiding this comment.
Reversign the direction here seems similarly undesirable, as obtain \<j, hj, rfl\> := comp_partial_sum_target_subset_image_comp_partial_sum_source _ _ _ i _, no longer works.
|
I have changed back the direction. If you are happy with this, you can merge yourself. |
|
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors merge |
|
Thanks! |
github-actions
bot
added
ready-to-merge
#6475) The old lemma combined a statement similar to `set.finite.image` with `set.finite.subset`. The new statement is a direct generalization of `set.finite.image`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
set.finite.dependent_imageset.finite.dependent_image
#6475) The old lemma combined a statement similar to `set.finite.image` with `set.finite.subset`. The new statement is a direct generalization of `set.finite.image`. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
The old lemma combined a statement similar to
set.finite.imagewithset.finite.subset. The new statement is a direct generalization ofset.finite.image.