-
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] - chore(measure_theory/pi): a few more lemmas #5604
Conversation
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
src/data/real/ennreal.lean
Outdated
@@ -748,6 +748,10 @@ section sum | |||
|
|||
open finset | |||
|
|||
/-- A product of finite numbers is still finite -/ | |||
lemma prod_lt_top {s : finset α} {f : α → ennreal} (h : ∀a∈s, f a < ∞) : (∏ a in s, f 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.
I thought that ≠ ∞
was the preferred way to write this in ennreal
? But if it's not standard, I'm happy to accept this, and try to uniformize this in a later PR.
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 data/real/ennreal
many lemmas are stated both for < ∞
and ≠ ∞
. Probably we should uniformize this at some point.
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
There is a merge conflict in bors d+ |
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Also prove that a locally finite measure in a `second_countable_topology` is `sigma_finite`.
Pull request successfully merged into master. Build succeeded: |
Also prove that a locally finite measure in a `second_countable_topology` is `sigma_finite`.
Also prove that a locally finite measure in a
second_countable_topology
issigma_finite
.ennreal.prod_lt_top
#5602set.pi
#5603