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

naming integral_sum #745

Closed
affeldt-aist opened this issue Sep 13, 2022 · 1 comment · Fixed by #767
Closed

naming integral_sum #745

affeldt-aist opened this issue Sep 13, 2022 · 1 comment · Fixed by #767
Milestone
0.6

Comments

@affeldt-aist
Copy link
Member

analysis/theories/lebesgue_integral.v

Lines 2074 to 2075 in d2ef896

Lemma integral_sum : \int[mu]_(x in D) (\sum_(n <oo) f n x) =
\sum_(n <oo) (\int[mu]_(x in D) (f n x)).

Maybe this should be ge0_integral_nnseries.
@affeldt-aist affeldt-aist added this to the 0.6 milestone Sep 13, 2022
@CohenCyril
Copy link
Member

Isn't the ge0 redundante with nn ??

affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Oct 7, 2022
@affeldt-aist
fixes math-comp#745
abd6955
@affeldt-aist affeldt-aist mentioned this issue Oct 7, 2022
Merged
1 task
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Oct 12, 2022
@affeldt-aist
fixes math-comp#745
7776095
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Oct 16, 2022
@affeldt-aist
fixes math-comp#745
ae16861
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Oct 20, 2022
@affeldt-aist
fixes math-comp#745
bffe427
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Oct 26, 2022
@affeldt-aist
fixes math-comp#745
8bef56a
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Nov 13, 2022
@affeldt-aist
fixes math-comp#745
18a6588
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Nov 23, 2022
@affeldt-aist
fixes math-comp#745
e45fa82
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Nov 25, 2022
@affeldt-aist
fixes math-comp#745
e4275ec
affeldt-aist added a commit that referenced this issue Nov 25, 2022
@affeldt-aist
fixes #745 (#767)
6cc1091 
* fixes #745

* Context rather than Variables
IshiguroYoshihiro pushed a commit to IshiguroYoshihiro/analysis that referenced this issue Dec 21, 2022
@affeldt-aist @IshiguroYoshihiro
fixes math-comp#745 (math-comp#767)
6a024c9 
* fixes math-comp#745

* Context rather than Variables
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
0.6
Development

Successfully merging a pull request may close this issue.

fixes #745 affeldt-aist/analysis
2 participants
@CohenCyril @affeldt-aist