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

express sup with supremum #489

Merged
merged 1 commit into from
Jun 8, 2022
Merged

express sup with supremum #489

merged 1 commit into from
Jun 8, 2022

Conversation

affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Dec 6, 2021 •
edited
Loading

The goal of this PR is to replace the definition of sup in reals.v by a definition using the more generic supremum from classical_sets.v. As a consequence, for example sup_out becomes a consequence of the properites of supremum and need not be axiomatized.

fixes #497

@affeldt-aist affeldt-aist force-pushed the sup_20211125 branch 2 times, most recently from a985308 to 10c8306 Compare December 13, 2021 09:05
@affeldt-aist affeldt-aist added this to the 0.4.1 milestone Feb 28, 2022
@affeldt-aist affeldt-aist mentioned this pull request Mar 7, 2022
Closed
@affeldt-aist affeldt-aist modified the milestones: 0.4.1, 0.4.2 Mar 22, 2022
CohenCyril
CohenCyril reviewed Apr 12, 2022
View reviewed changes
theories/reals.v Outdated Show resolved Hide resolved
@affeldt-aist
Copy link
Member Author

Could we merge this one on the grounds that it simplifies code a bit and provides documentation?
(It is my understanding that the blocking point is that lemmas in classical_sets.v could be better organized
to highlight the different side-conditions. Since it take time, we can maybe issue about that.)

@affeldt-aist affeldt-aist modified the milestones: 0.5.1, 0.5.2 Jun 3, 2022
CohenCyril
CohenCyril approved these changes Jun 7, 2022
View reviewed changes
Copy link
Member

@CohenCyril CohenCyril left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ok, sorry it took so much time

@affeldt-aist
express sup with supremum
2e8a2ce 
- complete documentation of `classical_sets.v`
- documentation of `reals.v`
- proof simplications in `reals.v`
  + `sup_out`, `sup0`, `sup1` now proved as consequences of the definition of `sup` using `supremum`
- minor generalizations
@affeldt-aist affeldt-aist merged commit 4cc17d8 into master Jun 8, 2022
@affeldt-aist affeldt-aist deleted the sup_20211125 branch June 8, 2022 09:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@CohenCyril CohenCyril CohenCyril approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
0.5.2
Development

Successfully merging this pull request may close these issues.

Doc of reals.v is missing
2 participants
@affeldt-aist @CohenCyril