-
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(data/list/lemmas): Range of foldr
#13328
Conversation
src/data/list/basic.lean
Outdated
@@ -2229,6 +2229,22 @@ begin | |||
apply hl _ (list.mem_cons_self _ _) } | |||
end | |||
|
|||
lemma foldr_range_subset_of_range_subset {f : α → γ → γ} {g : β → γ → γ} | |||
(hfg : set.range f ⊆ set.range g) (a) : set.range (foldr f a) ⊆ set.range (foldr g a) := |
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.
Is it the case that set.range (foldr f a) = ↑(submonoid.closure (range f) : submonoid (function.End γ))
?
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 can't get this statement to typecheck in Lean. But yes, set.range (foldr f a)
is the union of g a
for every g
in the monoid generated by the indexed family f
.
Should I prove this?
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 probably makes the dependencies difficult, so fine to do another time (if ever). It might be useful for your actual use-case though.
There is definitely a |
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.
Could you address Eric's suggestions?
bors d+ |
✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Build failed: |
This has been ported in the meantime. Could you open a matching mathlib4 PR? |
foldr
foldr
This has been moved to the bors r+ |
Mathlib4 pair: leanprover-community/mathlib4#1870 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Pull request successfully merged into master. Build succeeded: |
foldr
foldr
Mathlib3 pair: leanprover-community/mathlib#13328 Co-authored-by: Jon Eugster <eugster.jon@gmail.com>
Mathlib4 pair: leanprover-community/mathlib4#1870
These lemmas may seem super specific, but trust me, I do make use of them.
I don't believe there's a
foldl
analog to these lemmas, but I might be wrong.