Commit 2024-06-20 03:32 6e82bc0e

feat(Order/Maximal): maximality/minimality with insertion/removal for 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.