Nice name for a real (source code)

= Nice name for a real

For a forcing order with the <countable chain condition for forcing>, a real can be represented by a nice name determined by a countable <antichain in a forcing order> for each natural-number coordinate. This bounds the number of reals in the extension in terms of the size of the forcing order.