Skip to content

[Merged by Bors] - feat: prove Dini's theorem for uniform convergence#19068

Closed
j-loreaux wants to merge 23 commits intomasterfrom
j-loreaux/dini
Closed

[Merged by Bors] - feat: prove Dini's theorem for uniform convergence#19068
j-loreaux wants to merge 23 commits intomasterfrom
j-loreaux/dini

Conversation

@j-loreaux
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux commented Nov 15, 2024 •
edited by alreadydone
Loading

@j-loreaux j-loreaux added WIP Work in progress t-topology Topological spaces, uniform spaces, metric spaces, filters labels Nov 15, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 15, 2024 •
edited
Loading

PR summary 7de35ea251

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Topology.UniformSpace.Dini (new file) 1262

Declarations diff

+ OrderDual.instContinuousInv
+ OrderDual.instTopologicalGroup
+ OrderDual.instUniformSpace
+ tendsto_of_antitone_of_pointwise
+ tendsto_of_monotone_of_pointwise
++ tendstoLocallyUniformlyOn_of_forall_tendsto
++ tendstoLocallyUniformly_of_forall_tendsto
++ tendstoUniformlyOn_of_forall_tendsto
++ tendstoUniformly_of_forall_tendsto

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 15, 2024
@j-loreaux j-loreaux removed the WIP Work in progress label Nov 15, 2024
ADedecker
ADedecker reviewed Nov 15, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@ADedecker ADedecker left a comment

Choose a reason for hiding this comment

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

Thanks a lot!

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Nov 16, 2024
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Nov 16, 2024

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 16, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 16, 2024
ADedecker
ADedecker reviewed Nov 16, 2024
View reviewed changes
ADedecker
ADedecker reviewed Nov 16, 2024
View reviewed changes
urkud
urkud reviewed Nov 18, 2024
View reviewed changes
@j-loreaux @urkud
Update Mathlib/Topology/UniformSpace/Dini.lean
6490831 
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
ADedecker
ADedecker reviewed Nov 20, 2024
View reviewed changes
j-loreaux and others added 2 commits November 19, 2024 20:57
@j-loreaux @ADedecker
Update Mathlib/Topology/UniformSpace/Dini.lean
780cef5 
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
@j-loreaux @ADedecker
Update Mathlib/Topology/UniformSpace/Dini.lean
d783a1e 
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
YaelDillies
YaelDillies reviewed Dec 2, 2024
View reviewed changes
YaelDillies
YaelDillies approved these changes Dec 2, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Thanks!

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 2, 2024

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Dec 2, 2024
ADedecker
ADedecker reviewed Dec 2, 2024
View reviewed changes
@j-loreaux @ADedecker @YaelDillies
Apply suggestions from code review
7de35ea 
Co-authored-by: Anatole Dedecker <anatolededecker@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
jcommelin
jcommelin reviewed Dec 3, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Dec 3, 2024
mathlib-bors bot pushed a commit that referenced this pull request Dec 3, 2024
@j-loreaux
feat: prove Dini's theorem for uniform convergence (#19068)
0ddc4d7
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 3, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: prove Dini's theorem for uniform convergence [Merged by Bors] - feat: prove Dini's theorem for uniform convergence Dec 3, 2024
@mathlib-bors mathlib-bors bot closed this Dec 3, 2024
@mathlib-bors mathlib-bors bot deleted the j-loreaux/dini branch December 3, 2024 11:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@urkud urkud urkud left review comments

@jcommelin jcommelin jcommelin left review comments

@ADedecker ADedecker ADedecker left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. ready-to-merge This PR has been sent to bors. t-topology Topological spaces, uniform spaces, metric spaces, filters

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

7 participants

@j-loreaux @mathlib4-dependent-issues-bot @urkud @jcommelin @YaelDillies @ADedecker @leanprover-community-bot-assistant