Skip to content
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.

Sign up for GitHub

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

Jump to bottom

generalize ge0_integral_closed_ball #1299

Closed
affeldt-aist opened this issue Aug 22, 2024 · 0 comments · Fixed by #1302
Closed

generalize ge0_integral_closed_ball #1299

affeldt-aist opened this issue Aug 22, 2024 · 0 comments · Fixed by #1302
Labels
enhancement ✨ This issue/PR is about adding new features enhancing the library
Milestone
1.4.0

Comments

@affeldt-aist
Copy link
Member

analysis/theories/lebesgue_integral.v

Line 6361 in 7171aaf

Lemma ge0_integral_closed_ball (r : R) (r0 : (0 < r)%R) (f : R -> \bar R) :

does not need to be restricted to 0-centered balls
@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Aug 22, 2024
@affeldt-aist affeldt-aist added this to the 1.4.0 milestone Aug 22, 2024
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Aug 24, 2024
@affeldt-aist
fixes math-comp#1299
ae0f415
@affeldt-aist affeldt-aist mentioned this issue Aug 24, 2024
Merged
1 task
affeldt-aist added a commit that referenced this issue Aug 24, 2024
@affeldt-aist
fixes #1299 (#1302)
5c8f1fe
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement ✨ This issue/PR is about adding new features enhancing the library
Projects
None yet
Milestone
1.4.0
Development

Successfully merging a pull request may close this issue.

fixes #1299 (minor generalization) affeldt-aist/analysis
1 participant
@affeldt-aist