α : Type ?u.147716
r : α → α → Prop
o : Ordinal
h : ω ≤ o
⊢ IsRegular (succ (aleph' o))
α : Type ?u.147716
r : α → α → Prop
o : Ordinal
h : ω ≤ o
⊢ IsRegular (aleph' (succ o))
rw [aleph'_succ]
no goals
α : Type ?u.147716
r : α → α → Prop
o : Ordinal
h : ω ≤ o
⊢ IsRegular (succ (aleph' o))
exact isRegular_succ (aleph0_le_aleph'.2 h)