= Closed forcing adds no short ground-valued sequences
{title2=$({}^\alpha B)^M=({}^\alpha B)^{M[G]}$}
If a <forcing> is $\kappa$-closed in the ground model, then it adds no <functions> from a ground <ordinal> $\alpha<\kappa$ into a ground <set> $B$. Recursively decide each value inside the ground model and take common stronger bounds at limit stages and after the final step. Conditions deciding a whole ground <function> are dense below any condition asserting this type of <function>. The <dense-below generic meeting lemma> ensures the <generic filter> meets that <dense subset of a forcing order>. One arbitrary bound need not be in the <filter in an ordered set>.
Back to article page
