Skip to content

Bolzano weierstrass #1787

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
Open
affeldt-aist wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Bolzano weierstrass #1787

affeldt-aist wants to merge 4 commits into from
+123 −1

Conversation

@affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Dec 4, 2025 •
edited
Loading

Motivation for this change
Checklist
  • added corresponding entries in CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

CohenCyril
CohenCyril reviewed Dec 13, 2025
View reviewed changes
@affeldt-aist affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Dec 16, 2025
@affeldt-aist affeldt-aist added this to the 1.15.0 milestone Dec 16, 2025
@affeldt-aist affeldt-aist marked this pull request as ready for review December 16, 2025 04:57
@affeldt-aist
Copy link
Member Author

affeldt-aist commented Dec 23, 2025

At least, PR #1809 shows that this lemma is usable.

CohenCyril
CohenCyril reviewed Dec 26, 2025
View reviewed changes
theories/sequences.v
Qed.

Lemma finite_range_cvg (x_ : R ^nat) : finite_set (range x_) ->
Lemma finite_range_cst {T} (u_ : T^nat) : finite_set (range u_) ->
Copy link
Member

@CohenCyril CohenCyril Dec 26, 2025

Choose a reason for hiding this comment

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

probably the name should be finite_range_cst_subsequence or something like this.

CohenCyril
CohenCyril reviewed Dec 26, 2025
View reviewed changes
theories/sequences.v
by apply: sub_finite_set (Dfin x) => y /=; case: leP.
Qed.

Lemma finite_range_cvg {T : ptopologicalType} (x_ : T ^nat) :
Copy link
Member

@CohenCyril CohenCyril Dec 26, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

same ...cvg_subsequence or something like this

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@CohenCyril CohenCyril CohenCyril left review comments

Assignees

No one assigned

Labels

enhancement ✨ This issue/PR is about adding new features enhancing the library

Projects

None yet

Milestone

1.15.0

Development

Successfully merging this pull request may close these issues.

2 participants

@affeldt-aist @CohenCyril