We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 3f72762 commit 0b36773Copy full SHA for 0b36773
1 file changed
Mathlib/SetTheory/Cardinal/Aleph.lean
@@ -670,8 +670,8 @@ theorem lift_preBeth (o : Ordinal) : lift.{v} (preBeth o) = preBeth (Ordinal.lif
670
rw [mem_Iio, Ordinal.lift_lt] at hi
671
exact ⟨⟨i, hi⟩, IH _ hi⟩
672
673
-/-- The Beth function is defined so that `beth 0 = ℵ₀'`, `beth (succ o) = 2 ^ beth o`, and that for
674
-a limit ordinal `o`, `beth o` is the supremum of `beth a` for `a < o`.
+/-- 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`.
675
676
Assuming the generalized continuum hypothesis, which is undecidable in ZFC, we have `ℶ_ o = ℵ_ o`
677
for all ordinals.
0 commit comments