Stream: math-comp users

Topic: Type of powerset of a set


view this post on Zulip Julin Shaji (Mar 20 2024 at 05:34):

Is there a way to mention the type of the powerset of a set?

For example, type of set of booleans is [set bool].

Check [set true]: {set bool}.

Is there a way to express the type of sets whose elements are [set bool]?

Would this be a right way?

Check [set [set true]]: {set {set bool}}.

view this post on Zulip Quentin VERMANDE (Mar 20 2024 at 08:36):

Technically, the type of sets of booleans is {set bool}.
Regarding the powerset of a set, I assume you would like to have A : {set bool} and be able to write X : {set A}. This is not possible as of now because we would need a structure of finType on A, which we can not declare (afaict).
Regarding the type of sets whose elements are of type {set bool}, it is indeed {set {set bool}}.

view this post on Zulip Quentin VERMANDE (Mar 21 2024 at 08:25):

I just stumbled upon powerset, which might do what you want.


Last updated: Jul 15 2024 at 20:02 UTC