-
Notifications
You must be signed in to change notification settings - Fork 64
tentative formalization of Vitali's theorem #984
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
Conversation
d6256e9 to
03a4a02
Compare
6aababe to
9370cf1
Compare
6700d2c to
97749b3
Compare
97749b3 to
8bd4dc7
Compare
8bd4dc7 to
399200b
Compare
c264406 to
2793656
Compare
|
@zstone1 note that commit 2793656 turnes the lemma Lemma closed_disjoint_closed_ball {R : realFieldType} {M : normedModType R}
(K : set M) z (k : R) : closed K -> ~ K z -> 0 < k ->
exists2 d : {posnum R}, d%:num < k & closed_ball z d%:num `&` K = set0.into a Lemma closed_disjoint_closed_ball {R : realFieldType} {M : normedModType R}
(K : set M) z : closed K -> ~ K z ->
\forall d \near 0^'+, closed_ball z d `&` K = set0. |
|
The script for Vitali's theorem is far from being perfect but at least it is an application of the infinite case of Vitali's lemma. |
zstone1
left a comment
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.
One quick question about where the is_ball assumption goes, otherwise it's good.
d5d3b36 to
477fd54
Compare
477fd54 to
c46eb2e
Compare
* tentative formalization of Vitali's theorem --------- Co-authored-by: zstone1 <[email protected]>
* tentative formalization of Vitali's theorem --------- Co-authored-by: zstone1 <[email protected]>
Motivation for this change
based on PR #973
also duplicates code from a number of trivial PRs that should be merged first(PR #991 PR #992 PR #985 )Things done/to do
CHANGELOG_UNRELEASED.mdCompatibility with MathComp 2.0
TODO: HB portto make sure someone ports this PR tothe
hierarchy-builderbranch or I already opened an issue or PR (please cross reference).Automatic note to reviewers
Read this Checklist and put a milestone if possible.