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

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 κ

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.