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(topology/continuous_function): lemmas on infinite sums of continuous functions #18424
Conversation
/-- If `α` is locally compact, and an infinite sum of functions in `C(α, β)` | ||
converges to `g` (for the compact-open topology), then the pointwise sum converges to `g x` for | ||
all `x ∈ α`. -/ | ||
lemma has_sum_apply {α : Type*} {β : Type*} {γ : Type*} |
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 there a section you can place these in the file that already has three types with the right typeclasses?
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.
There wasn't, but there probably should have been (there was a long string of lemmas all repeating the declaration {α : Type*} {β : Type*} [topological_space α] [topological_space β]
each time). I've streamlined it a bit.
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.
Thanks 🎉
bors merge
Pull request successfully merged into master. Build succeeded: |
A lemma (in three variants) about evaluating infinite sums of continuous functions at a point. Split off from #18392.