[Merged by Bors] - feat(order/irreducible): Sup-irreducible elements #18999
Conversation
Define sup- and inf- irreducible and prime elements in a lattice.
YaelDillies
added
awaiting-review
github-actions
bot
added
the
modifies-synchronized-file
eric-wieser
added
the
not-too-late
|
|
||
| /-- A sup-irreducible element is a non-bottom element which isn't the supremum of anything smaller. | ||
| -/ | ||
| def sup_irred (a : α) : Prop := ¬ is_min a ∧ ∀ ⦃b c⦄, b ⊔ c = a → b = a ∨ c = a |
There was a problem hiding this comment.
This definition has the disadvantage of not working for finset α without decidable_eq α. Do you think that's worth a TODO?
There was a problem hiding this comment.
I doubt it really matters. Even though I will indeed set α := finset α in later code, this will be done in the context of category theory, where we don't have the luxury of restricting to types with decidable equality.
|
bors d+ |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
Is there any point keeping out-of-sync down now that it can't interfere with porting PRs? I'm going to assume that the answer is no. bors merge |
Define sup- and inf- irreducible and prime elements in a lattice.
|
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 sup- and inf- irreducible and prime elements in a lattice.