Constructible power set (source code)

= Constructible power set
{title2=$\mathcal P^L(A)$}

For $A\in L$, its constructible power set is
$$
\mathcal P^L(A)=\{X\in L:X\subseteq A\}=\mathcal P(A)\cap L.
$$
Unlike the single-stage <definable power set> $\mathcal D(A)$, it includes subsets of $A$ appearing arbitrarily late in the <constructible hierarchy>.