would it make sense to use the predicate `setI_closed` here?

[affeldt-aist]

analysis/classical/filter.v

Line 434 in 63a7b33

filterI : forall P Q : set T, F P -> F Q -> F (P `&` Q) ;

and also for opI in isOpenTopological, etc.

[t6s]

defining the filter type generally for lattices (not necessary set T) would make sense

[affeldt-aist]

oh, I was not envisioning so much refactoring, merely observing that a predicate we use a lot in measure theory could also be useful elsewhere

but maybe your remark could be a new issue for somebody to experiment, we can test together if we manage to find time