[Merged by Bors] - feat: Lattice closedness #7548
Conversation
Define when a set in a lattice is closed under lattice operations.
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
YaelDillies
added
awaiting-review
Mathlib/Order/SupClosed.lean
Outdated
|
|
||
| open Set | ||
|
|
||
| /-- A set `s` is *lattice-closed* if `a ⊔ b ∈ s` and `a ⊓ b ∈ s` for all `a ∈ s`, `b ∈ s`. -/ |
There was a problem hiding this comment.
Is this also the name used in the literature? Or does this concept not exist in the mainstream literature?
There was a problem hiding this comment.
This concept definitely exists in the literature: it's caled a sublattice. However I am trying to reserve this name for the bundled object, which I'm defining in #7549.
What do you think? Should I also say this is the property of being a sublattice? in the docstring or in the name?
There was a problem hiding this comment.
I would definitely mention this in the docstring. And I would even consider calling this isSublattice or something like that.
There was a problem hiding this comment.
I guess the argument for the current name is consistency with SupClosed and InfClosed.
There was a problem hiding this comment.
I've renamed it to IsSublattice for now.
leanprover-community-mathlib4-bot
added
ready-to-merge
Define when a set in a lattice is closed under lattice operations.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
Define when a set in a lattice is closed under lattice operations.
Define when a set in a lattice is closed under lattice operations.