Down filter

Back to Generic programming

A down filter is a pair of binary predicates on a preordered set `X`, called the element-filter and the down-set-filter. The element filter identifies a subset of `X`, called the marked elements. The down-set filter tells whether there are any marked elements in the principal down-set of a given element.

Theory

The down-set of a subset `S subset X` in `X` is the set

A subset `U subset X` is called a down-set if it is a down-set of some subset `S subset X`. A down-set is called principal if it is a down-set of a singular subset.

Remark 1.7.5 - Page generated 16.06.2017 01:37.