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.

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

Hb queue #1159

Merged
merged 6 commits into from
Jan 20, 2024
Merged

Hb queue #1159

merged 6 commits into from
Jan 20, 2024

Conversation

affeldt-aist
Copy link
Member

Motivation for this change

@zstone1 You may want to double check this commit before merge affeldt-aist@9fa2a1b

in the conversation of PR #926 you left this comment:
"The HB port should probably do two things

Define an alias for the compact-open topology, and build the topology on that.
Create a module which canonically assigns the compact-open topology to all the arrow types.

"
It is likely that I failed to implement it since I haven't created any module on purpose.

Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers
Compatibility with MathComp 2.0
  • I added the label TODO: HB port to make sure someone ports this PR to
    the hierarchy-builder branch or I already opened an issue or PR (please cross reference).
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

affeldt-aist and others added 6 commits January 18, 2024 12:34
* curry/uncurry of continuous functions

* compact-open topology working

* removing regular in favor of regular_space

---------

Co-authored-by: Reynald Affeldt <[email protected]>
Co-authored-by: Georges Gonthier <[email protected]>
* total variation proofs

- increasing implies BV
- splitting partitions
- right/left continuity of TV
- define variation with path
- adding monotone variation
- variation using prev and next

---------

Co-authored-by: Reynald Affeldt <[email protected]>
@proux01 proux01 merged commit 9258582 into math-comp:hierarchy-builder Jan 20, 2024
16 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants