Theorems · Definition · logic and foundations

Cardinal.beth

Ordinal.{u} → Cardinal.{u}

The Beth function is defined so that beth 0 = ℵ₀, beth (succ o) = 2 ^ beth o, and that for a limit ordinal o, beth o is the supremum of beth a for a < o. Assuming the generalized continuum hypothesis, which is undecidable in ZFC, we have ℶ_ o = ℵ_ o for all ordinals. For a version which starts at zero, see Cardinal.preBeth.

Defined in

Mathlib.SetTheory.Cardinal.Aleph

Cited by

35 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound