Cardinal arithmetic and cardinal characteristics
The arithmetic of infinite cardinals, including the continuum hypothesis and the singular cardinals hypothesis, together with cardinal invariants of the continuum and the cofinal structure of directed sets.
DefinitionSingular cardinals hypothesis#✓fully proved
MetaMathlibExt.SingularCardinalsHypothesis
For all singular cardinal \(\kappa\), if $2^{cof(\kappa)}\lt \kappa, then \(\kappa^{cof(\kappa)} = \kappa^+\).
def SingularCardinalsHypothesis.{u} : Prop :=
∀ κ : Cardinal.{u}, ℵ₀ ≤ κ → κ.ord.cof < κ →
(2 : Cardinal.{u}) ^ κ.ord.cof < κ → κ ^ κ.ord.cof = Order.succ κ
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.