fix #1863

[affeldt-aist]

Motivation for this change

fixes #1863

@t6s I was merely thinking of that

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[t6s]

Looks consistent and I approve this PR.

Is it good or bad to generalize this pattern into

Definition closed_under2 (T : Type) (p : pred T) (op : T -> T -> T) :=
  {in p &, forall x y, op x y \in p}.

and replace e.g. setU_closed by closed_under2 setU ?
(I noticed there are many *_closed in mathcomp.algebra.)

[t6s]

Another side note: filters of this form can be defined for any meet-semilattice, of which set _ is an instance; it can be even further generalized for posets, but in a slightly different form (meet-closedness replaced by downward directedness).

[CohenCyril]

We can merge as is and generalize (twice) as @t6s mentioned later on. BTW the reason why mathcomp algebra contains specific definition is because they are substructures, and indexing happens on a per structure basis as of now, and might be improvements by automatically generating morphisms and substructures as part of @VojtechStep work.

[CohenCyril]

and replace e.g. setU_closed by closed_under2 setU ?

We could even have the notation X.-closed2, we could do setU.-closed2 and downward.-closed2 where

Definition downward {L : porderType} {A : L} (B : L) (p : A <= B) : L := A.

[t6s]

improvements by automatically generating morphisms and substructures as part of @VojtechStep work.

sounds promising!

[CohenCyril]

@t6s would you be willing to open an issue based on our discussion here?

[affeldt-aist]

@t6s would you be willing to open an issue based on our discussion here?

i was apparently writing issue #1871 and #1872 while you were typing your message ;-)

[t6s]

reynald was so quick