[Merged by Bors] - feat(Topology/Order): existence of a sequence that converges to limsup by CoolRmal · Pull Request #37296 · leanprover-community/mathlib4

CoolRmal · 2026-03-28T01:03:00Z

The PR establishes the following results:

The limsSup of a filter f is a cluster point of f, and in fact it is the greatest cluster point of f.
If f is a countably generated filter in a first countable space, then there exists a sequence converging to limsSup f.
Analogous statements for limsup are also proved.
Analogous statements for limsInf and liminf are also proved.

Zulip discussion: #Is there code for X? > Existence of a subsequence that tendsto liminf

github-actions · 2026-03-28T01:04:08Z

PR summary 8db507d0c2

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ ClusterPt.le_limsSup
+ ClusterPt.limsInf
+ ClusterPt.limsInf_le
+ ClusterPt.limsSup
+ FirstCountableTopology.tendsto_subseq
+ MapClusterPt.le_limsup
+ MapClusterPt.liminf
+ MapClusterPt.liminf_le
+ MapClusterPt.limsup
+ _root_.ClusterPt.exists_seq_tendsto
+ _root_.MapClusterPt.exists_seq_tendsto
+ _root_.MapClusterPt.tendsto_subseq
+ exists_seq_comp_tendsto
+ exists_seq_tendsto_liminf
+ exists_seq_tendsto_limsInf
+ exists_seq_tendsto_limsSup
+ exists_seq_tendsto_limsup
+ isGreatest_clusterPt_limsSup
+ isGreatest_mapClusterPt_limsup
+ isLeast_clusterPt_limsInf
+ isLeast_mapClusterPt_liminf
- tendsto_subseq

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

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

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

Increase in tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type
6903	2	backward.isDefEq.respectTransparency

Current commit 88f412906a
Reference commit 8db507d0c2

You can run this locally as

./scripts/reporting/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).

Mathlib/Topology/Order/LiminfLimsup.lean

Co-authored-by: Snir Broshi <[email protected]>

Mathlib/Topology/Order/LiminfLimsup.lean

ADedecker

This looks good, thanks!

While you're at it, could you (in this PR or the next one) show that the limsInf of a (suitably bounded) filter is its least cluster point ? You've just proven that it is a cluster point, and then you can get that it's smaller than any cluster point using Filter.limsInf_le_limsInf_of_le and limsInf_eq_of_le_nhds.

Mathlib/Topology/Order/LiminfLimsup.lean

CoolRmal · 2026-03-29T21:04:03Z

-awaiting-author

Mathlib/Topology/Bases.lean

ADedecker

Thanks again, this looks very good. I think this will be the last round of review but I'll have a final look once you've made these changes.

Mathlib/Topology/Bases.lean

Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean

Mathlib/Topology/Bases.lean

Mathlib/Topology/Compactness/CountablyCompact.lean

Mathlib/Topology/Order/LiminfLimsup.lean

Co-authored-by: Anatole Dedecker <[email protected]>

…nto liminfsubseq

CoolRmal · 2026-04-03T01:45:46Z

-awaiting-author

@ADedecker Sorry for the delay. I think I’ve addressed all your comments. Could you take another look at this PR when you have time?

ADedecker

Thanks a lot, this looks very nice! Could you expand the PR description a bit?

bors d+

mathlib-bors · 2026-04-03T08:03:50Z

✌️ CoolRmal can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

CoolRmal · 2026-04-03T17:20:41Z

bors r+

#37296) The PR establishes the following results: 1. The `limsSup` of a filter `f` is a cluster point of `f`, and in fact it is the greatest cluster point of `f`. 2. If `f` is a countably generated filter in a first countable space, then there exists a sequence converging to `limsSup f`. 3. Analogous statements for `limsup` are also proved. 4. Analogous statements for `limsInf` and `liminf` are also proved. Zulip discussion: [#Is there code for X? > Existence of a subsequence that tendsto liminf](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Existence.20of.20a.20subsequence.20that.20tendsto.20liminf/with/582207405)

mathlib-bors · 2026-04-03T17:53:11Z

Pull request successfully merged into master.

Build succeeded:

Update LiminfLimsup.lean

804442e

github-actions bot added the t-topology Topological spaces, uniform spaces, metric spaces, filters label Mar 28, 2026

Update LiminfLimsup.lean

4e4f181

SnirBroshi reviewed Mar 28, 2026

View reviewed changes

CoolRmal mentioned this pull request Mar 28, 2026

[Merged by Bors] - feat(MeasureTheory): Fatou's lemma for countably generated filters #37313

Closed

1 task

CoolRmal and others added 2 commits March 28, 2026 08:20

Update Mathlib/Topology/Order/LiminfLimsup.lean

c8ed5af

Co-authored-by: Snir Broshi <[email protected]>

Update Mathlib/Topology/Order/LiminfLimsup.lean

0b06a92

Co-authored-by: Snir Broshi <[email protected]>

mathlib-triage bot assigned j-loreaux Mar 29, 2026

ADedecker reviewed Mar 29, 2026

View reviewed changes

Mathlib/Topology/Order/LiminfLimsup.lean Outdated Show resolved Hide resolved

ADedecker approved these changes Mar 29, 2026

View reviewed changes

Mathlib/Topology/Order/LiminfLimsup.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Order/LiminfLimsup.lean Outdated Show resolved Hide resolved

Mathlib/Topology/Order/LiminfLimsup.lean Outdated Show resolved Hide resolved

ADedecker added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 29, 2026

CoolRmal added 2 commits March 29, 2026 14:47

update

71177e8

update

6446519

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 29, 2026

fixdocstring

d484892

ADedecker reviewed Mar 29, 2026

View reviewed changes

Mathlib/Topology/Bases.lean Show resolved Hide resolved

CoolRmal added 3 commits March 29, 2026 21:20

deprecation

a1d9ed7

Update CountablyCompact.lean

e728bdf

Update CountablyCompact.lean

fae2367

ADedecker approved these changes Mar 30, 2026

View reviewed changes

ADedecker added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 30, 2026

CoolRmal and others added 7 commits April 2, 2026 19:33

Update Mathlib/Topology/Order/LiminfLimsup.lean

afd38b0

Co-authored-by: Anatole Dedecker <[email protected]>

Update Bases.lean

1a0d269

Merge branch 'liminfsubseq' of https://github.com/CoolRmal/mathlib4 i…

e1e3a3c

…nto liminfsubseq

Merge branch 'master' into liminfsubseq

31e690f

address comments

bb68313

Update LiminfLimsup.lean

17f5072

Update Sequences.lean

3aef770

Update Sequences.lean

29ef4b2

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 3, 2026

Update LiminfLimsup.lean

88f4129

ADedecker approved these changes Apr 3, 2026

View reviewed changes

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Apr 3, 2026

mathlib-bors bot changed the title ~~feat(Topology/Order): existence of a sequence that converges to limsup~~ [Merged by Bors] - feat(Topology/Order): existence of a sequence that converges to limsup Apr 3, 2026

mathlib-bors bot closed this Apr 3, 2026

CoolRmal deleted the liminfsubseq branch April 3, 2026 18:05

Conversation

CoolRmal commented Mar 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Mar 28, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8db507d0c2

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ADedecker left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

CoolRmal commented Mar 29, 2026

Uh oh!

Uh oh!

ADedecker left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

CoolRmal commented Apr 3, 2026

Uh oh!

ADedecker left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Apr 3, 2026

Uh oh!

CoolRmal commented Apr 3, 2026

Uh oh!

mathlib-bors bot commented Apr 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

CoolRmal commented Mar 28, 2026 •

edited

Loading

github-actions bot commented Mar 28, 2026 •

edited

Loading