[Merged by Bors] - feat(Order/Maximal): maximality/minimality with insertion/removal for sets#13638
[Merged by Bors] - feat(Order/Maximal): maximality/minimality with insertion/removal for sets#13638
Conversation
PR summary afc393f6ccImport changesDependency changes
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit> |
YaelDillies
left a comment
There was a problem hiding this comment.
I believe this is more generally true for P : α → Prop where α is a distributive atomic lattice ("proof": The same as your current proof, but with insert x s replaced by t = s ⊔ a such that s ⋖ t and a is an atom),
Do you think you could generalise (and then specialise back to Set and Finset)?
The right generality is really covers rather than unions with atoms, and it works in any order that is 'strongly atomic' (even non-lattice), which probably should get its own typeclass. For instance, it should be true for distributive + atomic or for modular + complemented + atomic, neither of which implies the other. I will add the finset versions, but I don't think a lattice version make sense until it has the right generality, which doesn't belong in this PR. |
YaelDillies
left a comment
There was a problem hiding this comment.
It is a bit problematic that you import finsets in a basic order theory file. Can you move the finset lemmas somewhere else?
I've moved them to |
|
bors merge |
… sets (#13638) We add a lemma showing that if `P` is a downwards-closed predicate on sets, then `s` is maximal w.r.t. `P` iff `s` has property `P` but no proper insertion of `s` has property `P`. We also add the dual lemma for single removals and upwards-closed predicates.
|
Pull request successfully merged into master. Build succeeded: |
… sets (#13638) We add a lemma showing that if `P` is a downwards-closed predicate on sets, then `s` is maximal w.r.t. `P` iff `s` has property `P` but no proper insertion of `s` has property `P`. We also add the dual lemma for single removals and upwards-closed predicates.
… sets (#13638) We add a lemma showing that if `P` is a downwards-closed predicate on sets, then `s` is maximal w.r.t. `P` iff `s` has property `P` but no proper insertion of `s` has property `P`. We also add the dual lemma for single removals and upwards-closed predicates.
… sets (#13638) We add a lemma showing that if `P` is a downwards-closed predicate on sets, then `s` is maximal w.r.t. `P` iff `s` has property `P` but no proper insertion of `s` has property `P`. We also add the dual lemma for single removals and upwards-closed predicates.
We add a lemma showing that if
Pis a downwards-closed predicate on sets, thensis maximal w.r.t.Piff
shas propertyPbut no proper insertion ofshas propertyP. We also add the dual lemma for single removals and upwards-closed predicates.