Skip to content

[Merged by Bors] - feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other iSup-like lemmas#15271

Closed
pechersky wants to merge 4 commits intomasterfrom
pechersky/ciSup-image
Closed

[Merged by Bors] - feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other iSup-like lemmas#15271
pechersky wants to merge 4 commits intomasterfrom
pechersky/ciSup-image

Conversation

@pechersky
Copy link
Copy Markdown
Contributor

@pechersky pechersky commented Jul 29, 2024

Open in Gitpod

@pechersky pechersky added the t-order Order theory label Jul 29, 2024
@github-actions
Copy link
Copy Markdown

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

PR summary 4fce318f48

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ ciInf_image
+ ciInf_subtype
+ ciInf_subtype'
+ ciInf_subtype''
+ ciSup_image
+ ciSup_or'
+ ciSup_subtype
+ ciSup_subtype'
+ ciSup_subtype''
+ csInf_image
+ csSup_image

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.

This was referenced Jul 29, 2024
Closed
Closed
eric-wieser
eric-wieser reviewed Jul 30, 2024
View reviewed changes
@pechersky @eric-wieser
Update Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
3af2662 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Ruben-VandeVelde
Ruben-VandeVelde reviewed Aug 2, 2024
View reviewed changes
pechersky and others added 2 commits August 2, 2024 12:24
@pechersky @Ruben-VandeVelde
Apply suggestions from code review
3393f39 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@pechersky
squeeze
4fce318
Ruben-VandeVelde
Ruben-VandeVelde approved these changes Aug 4, 2024
View reviewed changes
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

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

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 4, 2024

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 4, 2024
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Aug 5, 2024

Thanks!

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 5, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 5, 2024
@pechersky
feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other…
60be146 
… iSup-like lemmas (#15271)




Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 5, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Aug 5, 2024
@pechersky
feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other…
f74b424 
… iSup-like lemmas (#15271)




Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 5, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other iSup-like lemmas [Merged by Bors] - feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other iSup-like lemmas Aug 5, 2024
@mathlib-bors mathlib-bors bot closed this Aug 5, 2024
@mathlib-bors mathlib-bors bot deleted the pechersky/ciSup-image branch August 5, 2024 09:55
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@pechersky @bjoernkjoshanssen
feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other…
3917ea0 
… iSup-like lemmas (#15271)




Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
@pechersky @bjoernkjoshanssen
feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other…
97321fb 
… iSup-like lemmas (#15271)




Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
@pechersky @bjoernkjoshanssen
feat(ConditionallyCompleteLattice): ciSup_image, ciSup_or', and other…
08026b1 
… iSup-like lemmas (#15271)




Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde 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-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@pechersky @riccardobrasca @eric-wieser @Ruben-VandeVelde