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

gt0_fin_numE #1046

Closed
affeldt-aist opened this issue Oct 5, 2023 · 0 comments · Fixed by #1043
Closed

gt0_fin_numE #1046

affeldt-aist opened this issue Oct 5, 2023 · 0 comments · Fixed by #1043

Comments

@affeldt-aist
Copy link
Member

affeldt-aist commented Oct 5, 2023 •
edited
Loading

analysis/theories/constructive_ereal.v

Line 1468 in 9fbd7cd

Lemma ge0_fin_numE x : 0 <= x -> (x \is a fin_num) = (x < +oo).

it is really just a combination of ge0_fin_numE and ltW but since the name is so obvious, we could have it as well
@affeldt-aist affeldt-aist changed the title gt0_fin_num gt0_fin_numE Oct 5, 2023
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Oct 5, 2023
@affeldt-aist
fixes math-comp#1046
5fda5c1
@affeldt-aist affeldt-aist mentioned this issue Oct 5, 2023
Merged
2 tasks
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Oct 5, 2023
@affeldt-aist
fixes math-comp#1046
c134125
proux01 pushed a commit to affeldt-aist/analysis that referenced this issue Oct 9, 2023
@affeldt-aist @proux01
fixes math-comp#1046
3c56234
@proux01 proux01 closed this as completed in 86915bf Oct 9, 2023
affeldt-aist added a commit to affeldt-aist/analysis that referenced this issue Oct 10, 2023
@affeldt-aist
fixes math-comp#1046
59b9e14
affeldt-aist added a commit that referenced this issue Oct 11, 2023
@affeldt-aist
fixes #1046
d8955a7
IshiguroYoshihiro pushed a commit to IshiguroYoshihiro/analysis that referenced this issue Oct 24, 2023
@affeldt-aist @IshiguroYoshihiro
fixes math-comp#1046
04a6510
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
No milestone
Development

Successfully merging a pull request may close this issue.

Fixes 1042, 1037, 1045, 1046 affeldt-aist/analysis
1 participant
@affeldt-aist