Diamond theorem in the constructible universe (source code)

= Diamond theorem in the constructible universe
{title2=$L\models\diamondsuit$}

= Jensen diamond theorem
{c}
{synonym}

The <constructible universe> satisfies the <diamond principle>. Together with <antichain sealing by diamond>, this supplies a <Suslin tree> in $L$.