Skip to content

nondecreasing functions have a countable number of discontinuities#1451

Merged
CohenCyril merged 4 commits intomath-comp:masterfrom
affeldt-aist:discontinuities
Feb 5, 2025
Merged

nondecreasing functions have a countable number of discontinuities#1451
CohenCyril merged 4 commits intomath-comp:masterfrom
affeldt-aist:discontinuities

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
@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