α : Type ?u.147903
r : α → α → Prop
o : Ordinal
⊢ IsRegular (succ (aleph o))
α : Type ?u.147903
r : α → α → Prop
o : Ordinal
⊢ IsRegular (aleph (succ o))
rw [aleph_succ]
no goals
α : Type ?u.147903
r : α → α → Prop
o : Ordinal
⊢ IsRegular (succ (aleph o))
exact isRegular_succ (aleph0_le_aleph o)