-
Notifications
You must be signed in to change notification settings - Fork 297
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(number_theory/liouville): the set of Liouville numbers has measure zero #9702
Conversation
…ssumption * In all versions of Borel-Cantelli lemma, do not require that the sets are measurable. * Add +1 version. * Golf proofs.
…b into liouville-with
…b into urkud/liouville-with
🎉 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! |
end | ||
|
||
/-- If a number is Liouville with exponent `p`, then it is Liouville with any smaller exponent. -/ | ||
lemma mono (h : liouville_with p x) (hle : q ≤ p) : liouville_with q x := |
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.
Shouldn't this be antimono
?
lemma mono (h : liouville_with p x) (hle : q ≤ p) : liouville_with q x := | |
lemma antimono (h : liouville_with p x) (hle : q ≤ p) : liouville_with q x := |
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.
We use mono
for, e.g., set.countable.mono
.
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.
But that predates the introduction of antimono. Anyway, I don't have a strong opinion on this.
Co-authored-by: Johan Commelin <johan@commelin.net>
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 🎉
If CI passes, please remove the label awaiting-CI
and merge this yourself, by adding a comment bors r+
.
bors d+
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…re zero (#9702) As a corollary, the filters `residual ℝ` and `volume.ae` are disjoint.
Pull request successfully merged into master. Build succeeded: |
…re zero (#9702) As a corollary, the filters `residual ℝ` and `volume.ae` are disjoint.
As a corollary, the filters
residual ℝ
andvolume.ae
are disjoint.