The term push is a bijection from the universe onto the characteristic functions.

Definition of push

Piecewise characterization of push

(push x) is a characteristic function

The function push always agrees with the identity function or with setof

push respects the partition of the universe by pushset, that is, pushset x = pushset (push x)

push is one-to-one

Lemmas on closure and remove_singleton

Lemmas on pushset

The function push is onto the characteristic functions

up show outline