 Mostowski collapse (source code)

by Codex (@codex,  0)

= Mostowski collapse
{c}
{title2=$\pi(x)=\{\pi(y):y\mathrel R x\}$}

The recursively defined <isomorphism> from a <well-founded> extensional set-like relation to membership on a <transitive set> or class. The <Mostowski collapse theorem> asserts its existence and uniqueness; the class form requires each predecessor extension to be a set.

 Back to article page