Skip to content

[Merged by Bors] - feat(Topology/Algebra/Order/LiminfLimsup): generalize map liminf and map limsup lemmas#14591

Closed
kkytola wants to merge 17 commits intomasterfrom
kkytola/generalize_map_limsup_and_map_liminf
Closed

[Merged by Bors] - feat(Topology/Algebra/Order/LiminfLimsup): generalize map liminf and map limsup lemmas#14591
kkytola wants to merge 17 commits intomasterfrom
kkytola/generalize_map_limsup_and_map_liminf

Conversation

@kkytola
Copy link
Copy Markdown
Collaborator

@kkytola kkytola commented Jul 9, 2024 •
edited
Loading

Generalize map liminf and map limsup lemmas. Instead of assuming boundedness in both directions, it suffices to assume boundedness in one direction and coboundedness in the other direction.

This generalization resulted from a review comment of @sgouezel asking for the strenghtening of a specific ENNReal lemma about liminfs.

Open in Gitpod

@kkytola kkytola added WIP Work in progress t-topology Topological spaces, uniform spaces, metric spaces, filters t-order Order theory labels Jul 9, 2024
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 9, 2024 •
edited
Loading

PR summary 02931f23e7

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ Antitone.frequently_ge_map_of_frequently_le
+ Antitone.frequently_le_map_of_frequently_ge
+ Antitone.isCoboundedUnder_ge_of_isCobounded
+ Antitone.isCoboundedUnder_le_of_isCobounded
+ IsCobounded.frequently_ge
+ IsCobounded.frequently_le
+ IsCobounded.of_frequently_ge
+ IsCobounded.of_frequently_le
+ Monotone.frequently_ge_map_of_frequently_ge
+ Monotone.frequently_le_map_of_frequently_le
+ Monotone.isCoboundedUnder_ge_of_isCobounded
+ Monotone.isCoboundedUnder_le_of_isCobounded

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>

@kkytola kkytola removed the WIP Work in progress label Jul 10, 2024
@kkytola kkytola mentioned this pull request Jul 10, 2024
Closed
1 task
@urkud urkud requested a review from sgouezel July 13, 2024 14:37
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 13, 2024
kkytola added a commit that referenced this pull request Jul 13, 2024
@kkytola
Get the generalization of the liminf lemma from results in PR #14591.
2b915b7
kkytola added a commit that referenced this pull request Jul 13, 2024
@kkytola
Merge PR #14591.
8647ffa
@ghost ghost added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jul 13, 2024
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 21, 2024
kim-em
kim-em reviewed Jul 21, 2024
View reviewed changes
@kim-em kim-em added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 21, 2024
@kkytola kkytola removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 21, 2024
j-loreaux
j-loreaux reviewed Jul 21, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@j-loreaux j-loreaux left a comment

Choose a reason for hiding this comment

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

Thanks! This is a nice generalization.

@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 21, 2024
@kkytola kkytola removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 21, 2024
@j-loreaux j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 22, 2024
@kkytola kkytola removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 22, 2024
@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Jul 22, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 22, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 22, 2024
@kkytola
feat(Topology/Algebra/Order/LiminfLimsup): generalize map liminf and …
733640f 
…map limsup lemmas (#14591)

Generalize map liminf and map limsup lemmas. Instead of assuming boundedness in both directions, it suffices to assume boundedness in one direction and coboundedness in the other direction.



Co-authored-by: kkytola <“kalle.kytola@aalto.fi”>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 22, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Topology/Algebra/Order/LiminfLimsup): generalize map liminf and map limsup lemmas [Merged by Bors] - feat(Topology/Algebra/Order/LiminfLimsup): generalize map liminf and map limsup lemmas Jul 22, 2024
@mathlib-bors mathlib-bors bot closed this Jul 22, 2024
@mathlib-bors mathlib-bors bot deleted the kkytola/generalize_map_limsup_and_map_liminf branch July 22, 2024 20:53
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em left review comments

@j-loreaux j-loreaux j-loreaux left review comments

@sgouezel sgouezel Awaiting requested review from sgouezel

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-order Order theory 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.

3 participants

@kkytola @j-loreaux @kim-em