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

nondecreasing functions have a countable number of discontinuities #1451

Merged
merged 4 commits into from
Feb 5, 2025

Conversation

affeldt-aist
Copy link
Member

Motivation for this change

This comes from the development of the Banach-Zarecki proof.

@IshiguroYoshihiro

Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Jan 8, 2025
@affeldt-aist affeldt-aist added this to the 1.9.0 milestone Jan 8, 2025
classical/cardinality.v Outdated Show resolved Hide resolved
@affeldt-aist affeldt-aist force-pushed the discontinuities branch 2 times, most recently from dc06e3d to 953c67e Compare February 4, 2025 04:24
@affeldt-aist
Copy link
Member Author

I restored the infinite_set_fset lemma and cleaned up the scripts a bit (fixed indent, shortenings) but no substantial simplifications.

@affeldt-aist
Copy link
Member Author

@CohenCyril CI's green

@CohenCyril CohenCyril merged commit 212fca4 into math-comp:master Feb 5, 2025
32 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement ✨ This issue/PR is about adding new features enhancing the library
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants