Theorems · Definition · logic and foundations

Cardinal.preBeth

Ordinal.{u} → Cardinal.{u}

The "pre-beth" function is defined so that preBeth o is the supremum of 2 ^ preBeth a for a < o. This implies beth 0 = 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. For the usual function starting at ℵ₀, see Cardinal.beth.

Defined in

Mathlib.SetTheory.Cardinal.Aleph

Cited by

31 results in Mathlib

Foundations

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