Structure

covariant power set functor

Notation P∃:Set→SetP_{\exists}: \Set \to \Set Domain category of setsCodomain category of sets Related P∀P_{\forall} External nLab link
This functor P∃P_{\exists} maps a set XX to its power set P(X)P(X) and a map of sets f:X→Yf : X \to Y to the induced image operator f∗:P(X)→P(Y)f_* : P(X) \to P(Y).

Satisfied properties

Assigned properties

Deduced properties

Unsatisfied properties

Assigned properties

Deduced properties*

*This also uses the deduced satisfied properties.

Unknown properties

—

Undecidable properties

There is 1 property for which it cannot be decided whether it is satisfied.