Función de lavadero

En teoría de conjuntos , una función de Laver (o diamante de Laver , llamado así por su inventor, Richard Laver ) es una función relacionada con cardinales supercompactos .

Si κ es un cardinal supercompacto, una función de Laver es una función ƒ :κ  → V _κ tal que para cada conjunto x y cada cardinal λ ≥ |TC( x )| + κ existe una medida supercompacta U en [λ] ^<κ tal que si j _U es la incrustación elemental asociada, entonces j _U ( ƒ )(κ) = x . (Aquí V _κ denota el nivel κ de la jerarquía acumulativa , TC( x ) es la clausura transitiva de x )       

La aplicación original de las funciones de Laver fue el siguiente teorema de Laver. Si κ es supercompacto, existe una noción de forzamiento κ-cc ( P ,  ≤) tal que después de forzar con ( P ,  ≤) se cumple lo siguiente: κ es supercompacto y permanece supercompacto después de forzar con cualquier forzamiento cerrado dirigido por κ.

Existen muchas otras aplicaciones, por ejemplo, la demostración de la consistencia del axioma de forzamiento propio .