En la teoría de conjuntos , una función de Laver (o diamante de Laver , llamado así por su inventor, Richard Laver ) es una función conectada con cardinales supercompactos .
Si κ es un cardinal supercompacto, una función de Laver es una función ƒ :κ → V κ tal que para todo conjunto x y todo cardinal λ ≥ |TC( x )| + κ hay una medida supercompacta U en [λ] <κ tal que si j U es la incrustación elemental asociada entonces j U ( ƒ )(κ) = x . (Aquí V κ denota el κ-ésimo nivel de la jerarquía acumulativa , TC( x ) es el cierre transitivo 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 sigue siendo supercompacto después de forzar con cualquier forzamiento cerrado dirigido por κ.
Hay muchas otras aplicaciones, por ejemplo, la prueba de la consistencia del axioma de forzamiento adecuado .