-
Notifications
You must be signed in to change notification settings - Fork 299
[Merged by Bors] - chore(topology/algebra/infinite_sum): small todo #7994
Conversation
Heather, actually, this lemma was useful for the proof of the existence of Liouville numbers, but I have not worked on finishing those PRs in a while: go ahead with the change and I will get back to Liouville once I get a chance! |
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 am not sure that you prefer the exact terms, instead of the automated tactics, so feel free to disregard my suggestions!
Otherwise, this looks good to me!
(I am going to click on "Approve", just to see what it does, since I cannot really approve the changes anyway! (-: )
lemma has_sum_ite_eq_extract [decidable_eq β] (hf : has_sum f a) (b : β) : | ||
has_sum (λ n, ite (n = b) 0 (f n)) (a - f b) := | ||
begin | ||
convert has_sum_subtype_iff_indicator.mp (({b} : finset β).has_sum_iff_compl.mp hf), |
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.
In the original #6017 PR I suggested a proof that notes that has_sum (function.update f b 0)
is has_sum (λ n, ite (n = b) 0 (f n))
, and uses has_sum.update
. Does that proof work here?
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.
Probably (it'd be the same typeclass assumptions), but it doesn't seem like an obvious improvement?
Co-authored-by: damiano <adomani@gmail.com>
Thanks @adomani!
I think clicking "Approve" is about the same as saying "LGTM", both are useful flags for the maintainers! |
✌️ hrmacbeth can now approve this pull request. To approve and merge a pull request, simply reply with |
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+
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
bors r+ |
Build failed (retrying...): |
Pull request successfully merged into master. Build succeeded: |
Generalize a lemma from
f : ℕ → ℝ
tof : β → α
, withThis was marked as TODO after #6017/#6096.
@adomani, I assume this lemma is from the LTE. I hope the application there will work without change after this generalization, can you check?