Skip to content
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.

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

[Merged by Bors] - feat(order/(complete_lattice, compactly_generated)): independent sets in a complete lattice #5971

Closed
wants to merge 4 commits into from

Conversation

awainverse
Copy link
Collaborator

@awainverse awainverse commented Jan 30, 2021

Defines complete_lattice.independent
Shows that this notion of independence is finitary in compactly generated lattices


@awainverse awainverse added awaiting-review The author would like community review of the PR blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Jan 30, 2021
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Feb 2, 2021
@github-actions
Copy link

github-actions bot commented Feb 2, 2021

🎉 Great news! Looks like all the dependencies have been resolved:

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Feb 2, 2021
Copy link
Collaborator

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

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

Just a few dot notation golfs.

Thanks!
bors d+

src/order/compactly_generated.lean Outdated Show resolved Hide resolved
src/order/compactly_generated.lean Outdated Show resolved Hide resolved
src/order/complete_boolean_algebra.lean Outdated Show resolved Hide resolved
src/order/complete_boolean_algebra.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Feb 3, 2021

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

@bryangingechen bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Feb 3, 2021
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
@awainverse
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Feb 3, 2021
… in a complete lattice (#5971)

Defines `complete_lattice.independent`
Shows that this notion of independence is finitary in compactly generated lattices



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
@bors
Copy link

bors bot commented Feb 3, 2021

This PR was included in a batch that was canceled, it will be automatically retried

bors bot pushed a commit that referenced this pull request Feb 4, 2021
… in a complete lattice (#5971)

Defines `complete_lattice.independent`
Shows that this notion of independence is finitary in compactly generated lattices



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
@bors
Copy link

bors bot commented Feb 4, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(order/(complete_lattice, compactly_generated)): independent sets in a complete lattice [Merged by Bors] - feat(order/(complete_lattice, compactly_generated)): independent sets in a complete lattice Feb 4, 2021
@bors bors bot closed this Feb 4, 2021
@bors bors bot deleted the independent_lattice branch February 4, 2021 06:49
b-mehta pushed a commit that referenced this pull request Apr 2, 2021
… in a complete lattice (#5971)

Defines `complete_lattice.independent`
Shows that this notion of independence is finitary in compactly generated lattices



Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
bors bot pushed a commit that referenced this pull request Mar 21, 2022
…ependent` (#12588)

Putting this here means that in future we can talk about `pairwise_disjoint` at the same time, which was previously defined downstream of `complete_lattice.independent`.
This commit only moves existing declarations and adjusts module docstrings.

The new authorship comes from #5971 and #7199, which predate this file.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author A reviewer has asked the author a question or requested changes delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants